Theorem intssuni 4499

Description: The intersection of a nonempty set is a subclass of its union. (Contributed by NM, 29-Jul-2006.)

Assertion

Ref	Expression
intssuni	|- ( A =/= (/) -> |^| A C_ U. A )

Proof of Theorem intssuni

Dummy variables x y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		r19.2z 4060	. . . 4 |- ( ( A =/= (/) /\ A. y e. A x e. y ) -> E. y e. A x e. y )
2	1	ex 450	. . 3 |- ( A =/= (/) -> ( A. y e. A x e. y -> E. y e. A x e. y ) )
3		vex 3203	. . . 4 |- x e. _V
4	3	elint2 4482	. . 3 |- ( x e. |^| A <-> A. y e. A x e. y )
5		eluni2 4440	. . 3 |- ( x e. U. A <-> E. y e. A x e. y )
6	2, 4, 5	3imtr4g 285	. 2 |- ( A =/= (/) -> ( x e. |^| A -> x e. U. A ) )
7	6	ssrdv 3609	1 |- ( A =/= (/) -> |^| A C_ U. A )

Syntax hints:   -> wi 4   e. wcel 1990   =/= wne 2794   A.wral 2912   E.wrex 2913   C_ wss 3574   (/)c0 3915   U.cuni 4436   |^|cint 4475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-v 3202  df-dif 3577  df-in 3581  df-ss 3588  df-nul 3916  df-uni 4437  df-int 4476

This theorem is referenced by:  unissint  4501  intssuni2  4502  fin23lem31  9165  wunint  9537  tskint  9607  incexc  14569  incexc2  14570  subgint  17618  efgval  18130  lbsextlem3  19160  cssmre  20037  uffixfr  21727  uffix2  21728  uffixsn  21729  insiga  30200  dfon2lem8  31695  bj-intss  33053  intidl  33828  elrfi  37257