Theorem elunii 3980

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 2465	. . . . 5 |- ( x = B -> ( A e. x <-> A e. B ) )
2		eleq1 2464	. . . . 5 |- ( x = B -> ( x e. C <-> B e. C ) )
3	1, 2	anbi12d 692	. . . 4 |- ( x = B -> ( ( A e. x /\ x e. C ) <-> ( A e. B /\ B e. C ) ) )
4	3	spcegv 2997	. . 3 |- ( B e. C -> ( ( A e. B /\ B e. C ) -> E. x ( A e. x /\ x e. C ) ) )
5	4	anabsi7 793	. 2 |- ( ( A e. B /\ B e. C ) -> E. x ( A e. x /\ x e. C ) )
6		eluni 3978	. 2 |- ( A e. U. C <-> E. x ( A e. x /\ x e. C ) )
7	5, 6	sylibr 204	1 |- ( ( A e. B /\ B e. C ) -> A e. U. C )

Syntax hints:   -> wi 4   /\ wa 359   E.wex 1547   = wceq 1649   e. wcel 1721   U.cuni 3975

This theorem is referenced by:  ssuni  3997  unipw  4374  opeluu  4674  unon  4770  limuni3  4791  uniinqs  6943  trcl  7620  rankwflemb  7675  ac5num  7873  dfac3  7958  isf34lem4  8213  axcclem  8293  ttukeylem7  8351  brdom7disj  8365  brdom6disj  8366  wrdexb  11718  dprdfeq0  15535  tgss2  17007  ppttop  17026  isclo  17106  neips  17132  2ndcomap  17474  2ndcsep  17475  txkgen  17637  txcon  17674  basqtop  17696  nrmr0reg  17734  alexsublem  18028  alexsubALTlem4  18034  alexsubALT  18035  ptcmplem4  18039  unirnblps  18402  unirnbl  18403  blbas  18413  met2ndci  18505  bndth  18936  dyadmbllem  19444  opnmbllem  19446  dya2iocnei  24585  dstfrvunirn  24685  pconcon  24871  cvmcov2  24915  cvmlift2lem11  24953  cvmlift2lem12  24954  onint1  26103  mblfinlem  26143  locfincmp  26274  comppfsc  26277  neibastop2lem  26279  heibor1  26409  unichnidl  26531  prtlem16  26608  prter2  26620  stoweidlem43  27659  stoweidlem55  27671  truniALT  28337  unipwrVD  28653  unipwr  28654  truniALTVD  28699  unisnALT  28747

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-v 2918  df-uni 3976