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

Theorem elunii 3832
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 2344 . . . . 5  |-  ( x  =  B  ->  ( A  e.  x  <->  A  e.  B ) )
2 eleq1 2343 . . . . 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 2869 . . 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 3830 . 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 1528    = wceq 1623    e. wcel 1684   U.cuni 3827
This theorem is referenced by:  ssuni  3849  unipw  4224  opeluu  4526  unon  4622  limuni3  4643  trcl  7410  rankwflemb  7465  ac5num  7663  dfac3  7748  isf34lem4  8003  axcclem  8083  ttukeylem7  8142  brdom7disj  8156  brdom6disj  8157  wrdexb  11449  dprdfeq0  15257  tgss2  16725  ppttop  16744  isclo  16824  neips  16850  2ndcomap  17184  2ndcsep  17185  txkgen  17346  txcon  17383  basqtop  17402  nrmr0reg  17440  alexsublem  17738  alexsubALTlem4  17744  alexsubALT  17745  ptcmplem4  17749  unirnbl  17969  blbas  17976  met2ndci  18068  bndth  18456  dyadmbllem  18954  opnmbllem  18956  dstfrvunirn  23675  pconcon  23762  cvmcov2  23806  cvmlift2lem11  23844  cvmlift2lem12  23845  onint1  24888  uninqs  25039  osneisi  25531  bwt2  25592  locfincmp  26304  comppfsc  26307  neibastop2lem  26309  heibor1  26534  unichnidl  26656  prtlem16  26737  prter2  26749  stoweidlem43  27792  stoweidlem55  27804  truniALT  28305  unipwrVD  28608  unipwr  28609  truniALTVD  28654  unisnALT  28702
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-uni 3828
  Copyright terms: Public domain W3C validator