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

Theorem eluni 3960
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 2907 . 2  |-  ( A  e.  U. B  ->  A  e.  _V )
2 elex 2907 . . . 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 2447 . . . . 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 3958 . . 3  |-  U. B  =  { y  |  E. x ( y  e.  x  /\  x  e.  B ) }
97, 8elab2g 3027 . 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 1717   _Vcvv 2899   U.cuni 3957
This theorem is referenced by:  eluni2  3961  elunii  3962  eluniab  3969  uniun  3976  uniin  3977  uniss  3978  unissb  3987  dftr2  4245  unipw  4355  uniex2  4644  uniuni  4656  dmuni  5019  fununi  5457  elunirnALT  5939  mpt2xopxnop0  6402  tfrlem7  6580  tfrlem9a  6583  inf2  7511  inf3lem2  7517  rankwflemb  7652  cardprclem  7799  carduni  7801  iunfictbso  7928  kmlem3  7965  kmlem4  7966  cfub  8062  isf34lem4  8190  grothtsk  8643  suplem1pr  8862  isbasis2g  16936  tgval2  16944  ntreq0  17064  cmpsublem  17384  cmpsub  17385  cmpcld  17387  is1stc2  17426  alexsubALTlem3  18001  alexsubALT  18003  wfrlem11  25290  frrlem5c  25311  fnessref  26064  elunif  27355  stoweidlem27  27444  stoweidlem48  27465  truniALT  27969  truniALTVD  28331  unisnALT  28379
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 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-v 2901  df-uni 3958
  Copyright terms: Public domain W3C validator