Theorem elunii 4227

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 2502	. . . . 5 |- ( x = B -> ( A e. x <-> A e. B ) )
2		eleq1 2501	. . . . 5 |- ( x = B -> ( x e. C <-> B e. C ) )
3	1, 2	anbi12d 715	. . . 4 |- ( x = B -> ( ( A e. x /\ x e. C ) <-> ( A e. B /\ B e. C ) ) )
4	3	spcegv 3173	. . 3 |- ( B e. C -> ( ( A e. B /\ B e. C ) -> E. x ( A e. x /\ x e. C ) ) )
5	4	anabsi7 826	. 2 |- ( ( A e. B /\ B e. C ) -> E. x ( A e. x /\ x e. C ) )
6		eluni 4225	. 2 |- ( A e. U. C <-> E. x ( A e. x /\ x e. C ) )
7	5, 6	sylibr 215	1 |- ( ( A e. B /\ B e. C ) -> A e. U. C )

Syntax hints:   -> wi 4   /\ wa 370   = wceq 1437   E.wex 1659   e. wcel 1870   U.cuni 4222

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407

This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-v 3089  df-uni 4223

This theorem is referenced by:  ssuni  4244  unipw  4672  opeluu  4691  unon  6672  limuni3  6693  uniinqs  7451  trcl  8211  rankwflemb  8263  ac5num  8465  dfac3  8550  isf34lem4  8805  axcclem  8885  ttukeylem7  8943  brdom7disj  8957  brdom6disj  8958  wrdexb  12670  dprdfeq0  17590  tgss2  19934  ppttop  19953  isclo  20034  neips  20060  2ndcomap  20404  2ndcsep  20405  locfincmp  20472  comppfsc  20478  txkgen  20598  txcon  20635  basqtop  20657  nrmr0reg  20695  alexsublem  20990  alexsubALTlem4  20996  alexsubALT  20997  ptcmplem4  21001  unirnblps  21365  unirnbl  21366  blbas  21376  met2ndci  21468  bndth  21882  dyadmbllem  22434  opnmbllem  22436  dya2iocnei  28943  dstfrvunirn  29133  pconcon  29742  cvmcov2  29786  cvmlift2lem11  29824  cvmlift2lem12  29825  neibastop2lem  30801  onint1  30894  icoreunrn  31496  opnmbllem0  31680  heibor1  31846  unichnidl  31968  prtlem16  32149  prter2  32161  truniALT  36539  unipwrVD  36868  unipwr  36869  truniALTVD  36915  unisnALT  36963  disjinfi  37091  stoweidlem43  37473  stoweidlem55  37485