Theorem elunii 4250

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 2540	. . . . 5 |- ( x = B -> ( A e. x <-> A e. B ) )
2		eleq1 2539	. . . . 5 |- ( x = B -> ( x e. C <-> B e. C ) )
3	1, 2	anbi12d 710	. . . 4 |- ( x = B -> ( ( A e. x /\ x e. C ) <-> ( A e. B /\ B e. C ) ) )
4	3	spcegv 3199	. . 3 |- ( B e. C -> ( ( A e. B /\ B e. C ) -> E. x ( A e. x /\ x e. C ) ) )
5	4	anabsi7 817	. 2 |- ( ( A e. B /\ B e. C ) -> E. x ( A e. x /\ x e. C ) )
6		eluni 4248	. 2 |- ( A e. U. C <-> E. x ( A e. x /\ x e. C ) )
7	5, 6	sylibr 212	1 |- ( ( A e. B /\ B e. C ) -> A e. U. C )

Syntax hints:   -> wi 4   /\ wa 369   = wceq 1379   E.wex 1596   e. wcel 1767   U.cuni 4245

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-uni 4246

This theorem is referenced by:  ssuni  4267  unipw  4697  opeluu  4716  unon  6650  limuni3  6671  uniinqs  7391  trcl  8159  rankwflemb  8211  ac5num  8417  dfac3  8502  isf34lem4  8757  axcclem  8837  ttukeylem7  8895  brdom7disj  8909  brdom6disj  8910  wrdexb  12524  dprdfeq0  16864  dprdfeq0OLD  16871  tgss2  19283  ppttop  19302  isclo  19382  neips  19408  bwthOLD  19705  2ndcomap  19753  2ndcsep  19754  txkgen  19916  txcon  19953  basqtop  19975  nrmr0reg  20013  alexsublem  20307  alexsubALTlem4  20313  alexsubALT  20314  ptcmplem4  20318  unirnblps  20685  unirnbl  20686  blbas  20696  met2ndci  20788  bndth  21221  dyadmbllem  21771  opnmbllem  21773  dya2iocnei  27921  dstfrvunirn  28081  pconcon  28344  cvmcov2  28388  cvmlift2lem11  28426  cvmlift2lem12  28427  onint1  29519  opnmbllem0  29655  locfincmp  29804  comppfsc  29807  neibastop2lem  29809  heibor1  29937  unichnidl  30059  prtlem16  30242  prter2  30254  stoweidlem43  31371  stoweidlem55  31383  truniALT  32410  unipwrVD  32730  unipwr  32731  truniALTVD  32776  unisnALT  32824