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

Theorem elunii 3848
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 2357 . . . . 5  |-  ( x  =  B  ->  ( A  e.  x  <->  A  e.  B ) )
2 eleq1 2356 . . . . 5  |-  ( x  =  B  ->  (
x  e.  C  <->  B  e.  C ) )
31, 2anbi12d 691 . . . 4  |-  ( x  =  B  ->  (
( A  e.  x  /\  x  e.  C
)  <->  ( A  e.  B  /\  B  e.  C ) ) )
43spcegv 2882 . . 3  |-  ( B  e.  C  ->  (
( A  e.  B  /\  B  e.  C
)  ->  E. x
( A  e.  x  /\  x  e.  C
) ) )
54anabsi7 792 . 2  |-  ( ( A  e.  B  /\  B  e.  C )  ->  E. x ( A  e.  x  /\  x  e.  C ) )
6 eluni 3846 . 2  |-  ( A  e.  U. C  <->  E. x
( A  e.  x  /\  x  e.  C
) )
75, 6sylibr 203 1  |-  ( ( A  e.  B  /\  B  e.  C )  ->  A  e.  U. C
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358   E.wex 1531    = wceq 1632    e. wcel 1696   U.cuni 3843
This theorem is referenced by:  ssuni  3865  unipw  4240  opeluu  4542  unon  4638  limuni3  4659  trcl  7426  rankwflemb  7481  ac5num  7679  dfac3  7764  isf34lem4  8019  axcclem  8099  ttukeylem7  8158  brdom7disj  8172  brdom6disj  8173  wrdexb  11465  dprdfeq0  15273  tgss2  16741  ppttop  16760  isclo  16840  neips  16866  2ndcomap  17200  2ndcsep  17201  txkgen  17362  txcon  17399  basqtop  17418  nrmr0reg  17456  alexsublem  17754  alexsubALTlem4  17760  alexsubALT  17761  ptcmplem4  17765  unirnbl  17985  blbas  17992  met2ndci  18084  bndth  18472  dyadmbllem  18970  opnmbllem  18972  dstfrvunirn  23690  pconcon  23777  cvmcov2  23821  cvmlift2lem11  23859  cvmlift2lem12  23860  onint1  24960  uninqs  25142  osneisi  25634  bwt2  25695  locfincmp  26407  comppfsc  26410  neibastop2lem  26412  heibor1  26637  unichnidl  26759  prtlem16  26840  prter2  26852  stoweidlem43  27895  stoweidlem55  27907  truniALT  28604  unipwrVD  28924  unipwr  28925  truniALTVD  28970  unisnALT  29018
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-uni 3844
  Copyright terms: Public domain W3C validator