MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elunii Structured version   Unicode version

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.
StepHypRef 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 ) )
31, 2anbi12d 715 . . . 4  |-  ( x  =  B  ->  (
( A  e.  x  /\  x  e.  C
)  <->  ( A  e.  B  /\  B  e.  C ) ) )
43spcegv 3173 . . 3  |-  ( B  e.  C  ->  (
( A  e.  B  /\  B  e.  C
)  ->  E. x
( A  e.  x  /\  x  e.  C
) ) )
54anabsi7 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
) )
75, 6sylibr 215 1  |-  ( ( A  e.  B  /\  B  e.  C )  ->  A  e.  U. C
)
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator