Theorem elunii 4093

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 705	. . . 4 |- ( x = B -> ( ( A e. x /\ x e. C ) <-> ( A e. B /\ B e. C ) ) )
4	3	spcegv 3055	. . 3 |- ( B e. C -> ( ( A e. B /\ B e. C ) -> E. x ( A e. x /\ x e. C ) ) )
5	4	anabsi7 810	. 2 |- ( ( A e. B /\ B e. C ) -> E. x ( A e. x /\ x e. C ) )
6		eluni 4091	. 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 1364   E.wex 1591   e. wcel 1761   U.cuni 4088

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-v 2972  df-uni 4089

This theorem is referenced by:  ssuni  4110  unipw  4539  opeluu  4558  unon  6441  limuni3  6462  uniinqs  7176  trcl  7944  rankwflemb  7996  ac5num  8202  dfac3  8287  isf34lem4  8542  axcclem  8622  ttukeylem7  8680  brdom7disj  8694  brdom6disj  8695  wrdexb  12241  dprdfeq0  16502  dprdfeq0OLD  16509  tgss2  18492  ppttop  18511  isclo  18591  neips  18617  bwthOLD  18914  2ndcomap  18962  2ndcsep  18963  txkgen  19125  txcon  19162  basqtop  19184  nrmr0reg  19222  alexsublem  19516  alexsubALTlem4  19522  alexsubALT  19523  ptcmplem4  19527  unirnblps  19894  unirnbl  19895  blbas  19905  met2ndci  19997  bndth  20430  dyadmbllem  20979  opnmbllem  20981  dya2iocnei  26617  dstfrvunirn  26771  pconcon  27034  cvmcov2  27078  cvmlift2lem11  27116  cvmlift2lem12  27117  onint1  28209  opnmbllem0  28336  locfincmp  28485  comppfsc  28488  neibastop2lem  28490  heibor1  28618  unichnidl  28740  prtlem16  28923  prter2  28935  stoweidlem43  29747  stoweidlem55  29759  truniALT  31064  unipwrVD  31385  unipwr  31386  truniALTVD  31431  unisnALT  31479