Theorem elunii 4224

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 2496	. . . . 5 |- ( x = B -> ( A e. x <-> A e. B ) )
2		eleq1 2495	. . . . 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 3167	. . 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 4222	. 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 1657   e. wcel 1872   U.cuni 4219

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401

This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-v 3082  df-uni 4220

This theorem is referenced by:  ssuni  4241  unipw  4671  opeluu  4690  unon  6673  limuni3  6694  uniinqs  7455  trcl  8221  rankwflemb  8273  ac5num  8475  dfac3  8560  isf34lem4  8815  axcclem  8895  ttukeylem7  8953  brdom7disj  8967  brdom6disj  8968  wrdexb  12688  dprdfeq0  17655  tgss2  20002  ppttop  20021  isclo  20102  neips  20128  2ndcomap  20472  2ndcsep  20473  locfincmp  20540  comppfsc  20546  txkgen  20666  txcon  20703  basqtop  20725  nrmr0reg  20763  alexsublem  21058  alexsubALTlem4  21064  alexsubALT  21065  ptcmplem4  21069  unirnblps  21433  unirnbl  21434  blbas  21444  met2ndci  21536  bndth  21985  dyadmbllem  22556  opnmbllem  22558  dya2iocnei  29113  dstfrvunirn  29316  pconcon  29963  cvmcov2  30007  cvmlift2lem11  30045  cvmlift2lem12  30046  neibastop2lem  31022  onint1  31115  icoreunrn  31727  opnmbllem0  31941  heibor1  32107  unichnidl  32229  prtlem16  32410  prter2  32422  truniALT  36873  unipwrVD  37202  unipwr  37203  truniALTVD  37249  unisnALT  37297  disjinfi  37430  stoweidlem43  37845  stoweidlem55  37857