Theorem elunii 4217

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 2529	. . . . 5 |- ( x = B -> ( A e. x <-> A e. B ) )
2		eleq1 2528	. . . . 5 |- ( x = B -> ( x e. C <-> B e. C ) )
3	1, 2	anbi12d 722	. . . 4 |- ( x = B -> ( ( A e. x /\ x e. C ) <-> ( A e. B /\ B e. C ) ) )
4	3	spcegv 3147	. . 3 |- ( B e. C -> ( ( A e. B /\ B e. C ) -> E. x ( A e. x /\ x e. C ) ) )
5	4	anabsi7 833	. 2 |- ( ( A e. B /\ B e. C ) -> E. x ( A e. x /\ x e. C ) )
6		eluni 4215	. 2 |- ( A e. U. C <-> E. x ( A e. x /\ x e. C ) )
7	5, 6	sylibr 217	1 |- ( ( A e. B /\ B e. C ) -> A e. U. C )

Syntax hints:   -> wi 4   /\ wa 375   = wceq 1455   E.wex 1674   e. wcel 1898   U.cuni 4212

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442

This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-v 3059  df-uni 4213

This theorem is referenced by:  ssuni  4234  unipw  4667  opeluu  4688  unon  6690  limuni3  6711  uniinqs  7474  trcl  8243  rankwflemb  8295  ac5num  8498  dfac3  8583  isf34lem4  8838  axcclem  8918  ttukeylem7  8976  brdom7disj  8990  brdom6disj  8991  wrdexb  12722  dprdfeq0  17710  tgss2  20058  ppttop  20077  isclo  20158  neips  20184  2ndcomap  20528  2ndcsep  20529  locfincmp  20596  comppfsc  20602  txkgen  20722  txcon  20759  basqtop  20781  nrmr0reg  20819  alexsublem  21114  alexsubALTlem4  21120  alexsubALT  21121  ptcmplem4  21125  unirnblps  21489  unirnbl  21490  blbas  21500  met2ndci  21592  bndth  22041  dyadmbllem  22613  opnmbllem  22615  dya2iocnei  29154  dstfrvunirn  29357  pconcon  30004  cvmcov2  30048  cvmlift2lem11  30086  cvmlift2lem12  30087  neibastop2lem  31066  onint1  31159  icoreunrn  31808  opnmbllem0  32022  heibor1  32188  unichnidl  32310  prtlem16  32487  prter2  32499  truniALT  36947  unipwrVD  37269  unipwr  37270  truniALTVD  37316  unisnALT  37364  disjinfi  37522  stoweidlem43  38005  stoweidlem55  38017  salexct  38294