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

Theorem eluni 3978
Description: Membership in class union. (Contributed by NM, 22-May-1994.)
Assertion
Ref Expression
eluni  |-  ( A  e.  U. B  <->  E. x
( A  e.  x  /\  x  e.  B
) )
Distinct variable groups:    x, A    x, B

Proof of Theorem eluni
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 elex 2924 . 2  |-  ( A  e.  U. B  ->  A  e.  _V )
2 elex 2924 . . . 4  |-  ( A  e.  x  ->  A  e.  _V )
32adantr 452 . . 3  |-  ( ( A  e.  x  /\  x  e.  B )  ->  A  e.  _V )
43exlimiv 1641 . 2  |-  ( E. x ( A  e.  x  /\  x  e.  B )  ->  A  e.  _V )
5 eleq1 2464 . . . . 5  |-  ( y  =  A  ->  (
y  e.  x  <->  A  e.  x ) )
65anbi1d 686 . . . 4  |-  ( y  =  A  ->  (
( y  e.  x  /\  x  e.  B
)  <->  ( A  e.  x  /\  x  e.  B ) ) )
76exbidv 1633 . . 3  |-  ( y  =  A  ->  ( E. x ( y  e.  x  /\  x  e.  B )  <->  E. x
( A  e.  x  /\  x  e.  B
) ) )
8 df-uni 3976 . . 3  |-  U. B  =  { y  |  E. x ( y  e.  x  /\  x  e.  B ) }
97, 8elab2g 3044 . 2  |-  ( A  e.  _V  ->  ( A  e.  U. B  <->  E. x
( A  e.  x  /\  x  e.  B
) ) )
101, 4, 9pm5.21nii 343 1  |-  ( A  e.  U. B  <->  E. x
( A  e.  x  /\  x  e.  B
) )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    /\ wa 359   E.wex 1547    = wceq 1649    e. wcel 1721   _Vcvv 2916   U.cuni 3975
This theorem is referenced by:  eluni2  3979  elunii  3980  eluniab  3987  uniun  3994  uniin  3995  uniss  3996  unissb  4005  dftr2  4264  unipw  4374  uniex2  4663  uniuni  4675  dmuni  5038  fununi  5476  elunirnALT  5959  mpt2xopxnop0  6425  tfrlem7  6603  tfrlem9a  6606  inf2  7534  inf3lem2  7540  rankwflemb  7675  cardprclem  7822  carduni  7824  iunfictbso  7951  kmlem3  7988  kmlem4  7989  cfub  8085  isf34lem4  8213  grothtsk  8666  suplem1pr  8885  isbasis2g  16968  tgval2  16976  ntreq0  17096  cmpsublem  17416  cmpsub  17417  cmpcld  17419  is1stc2  17458  alexsubALTlem3  18033  alexsubALT  18035  wfrlem11  25480  frrlem5c  25501  fnessref  26263  elunif  27554  stoweidlem27  27643  stoweidlem48  27664  truniALT  28337  truniALTVD  28699  unisnALT  28747
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-v 2918  df-uni 3976
  Copyright terms: Public domain W3C validator