Theorem elunii 4441

Description: Membership in class union. (Contributed by NM, 24-Mar-1995.)

Assertion

Ref	Expression
elunii	|- ( ( A e. B /\ B e. C ) -> A e. U. C )

Proof of Theorem elunii

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eleq2 2690	. . . . 5 |- ( x = B -> ( A e. x <-> A e. B ) )
2		eleq1 2689	. . . . 5 |- ( x = B -> ( x e. C <-> B e. C ) )
3	1, 2	anbi12d 747	. . . 4 |- ( x = B -> ( ( A e. x /\ x e. C ) <-> ( A e. B /\ B e. C ) ) )
4	3	spcegv 3294	. . 3 |- ( B e. C -> ( ( A e. B /\ B e. C ) -> E. x ( A e. x /\ x e. C ) ) )
5	4	anabsi7 860	. 2 |- ( ( A e. B /\ B e. C ) -> E. x ( A e. x /\ x e. C ) )
6		eluni 4439	. 2 |- ( A e. U. C <-> E. x ( A e. x /\ x e. C ) )
7	5, 6	sylibr 224	1 |- ( ( A e. B /\ B e. C ) -> A e. U. C )

Syntax hints:   -> wi 4   /\ wa 384   = wceq 1483   E.wex 1704   e. wcel 1990   U.cuni 4436

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-v 3202  df-uni 4437

This theorem is referenced by:  ssuni  4459  ssuniOLD  4460  unipw  4918  opeluu  4939  unon  7031  limuni3  7052  uniinqs  7827  trcl  8604  rankwflemb  8656  ac5num  8859  dfac3  8944  isf34lem4  9199  axcclem  9279  ttukeylem7  9337  brdom7disj  9353  brdom6disj  9354  wrdexb  13316  dprdfeq0  18421  tgss2  20791  ppttop  20811  isclo  20891  neips  20917  2ndcomap  21261  2ndcsep  21262  locfincmp  21329  comppfsc  21335  txkgen  21455  txconn  21492  basqtop  21514  nrmr0reg  21552  alexsublem  21848  alexsubALTlem4  21854  alexsubALT  21855  ptcmplem4  21859  unirnblps  22224  unirnbl  22225  blbas  22235  met2ndci  22327  bndth  22757  dyadmbllem  23367  opnmbllem  23369  dya2iocnei  30344  dstfrvunirn  30536  pconnconn  31213  cvmcov2  31257  cvmlift2lem11  31295  cvmlift2lem12  31296  neibastop2lem  32355  onint1  32448  icoreunrn  33207  opnmbllem0  33445  heibor1  33609  unichnidl  33830  prtlem16  34154  prter2  34166  truniALT  38751  unipwrVD  39067  unipwr  39068  truniALTVD  39114  unisnALT  39162  restuni3  39301  disjinfi  39380  stoweidlem43  40260  stoweidlem55  40272  salexct  40552