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

Theorem eluni 4010
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 2956 . 2  |-  ( A  e.  U. B  ->  A  e.  _V )
2 elex 2956 . . . 4  |-  ( A  e.  x  ->  A  e.  _V )
32adantr 452 . . 3  |-  ( ( A  e.  x  /\  x  e.  B )  ->  A  e.  _V )
43exlimiv 1644 . 2  |-  ( E. x ( A  e.  x  /\  x  e.  B )  ->  A  e.  _V )
5 eleq1 2495 . . . . 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 1636 . . 3  |-  ( y  =  A  ->  ( E. x ( y  e.  x  /\  x  e.  B )  <->  E. x
( A  e.  x  /\  x  e.  B
) ) )
8 df-uni 4008 . . 3  |-  U. B  =  { y  |  E. x ( y  e.  x  /\  x  e.  B ) }
97, 8elab2g 3076 . 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 1550    = wceq 1652    e. wcel 1725   _Vcvv 2948   U.cuni 4007
This theorem is referenced by:  eluni2  4011  elunii  4012  eluniab  4019  uniun  4026  uniin  4027  uniss  4028  unissb  4037  dftr2  4296  unipw  4406  uniex2  4696  uniuni  4708  dmuni  5071  fununi  5509  elunirnALT  5992  mpt2xopxnop0  6458  tfrlem7  6636  tfrlem9a  6639  inf2  7570  inf3lem2  7576  rankwflemb  7711  cardprclem  7858  carduni  7860  iunfictbso  7987  kmlem3  8024  kmlem4  8025  cfub  8121  isf34lem4  8249  grothtsk  8702  suplem1pr  8921  isbasis2g  17005  tgval2  17013  ntreq0  17133  cmpsublem  17454  cmpsub  17455  cmpcld  17457  is1stc2  17497  alexsubALTlem3  18072  alexsubALT  18074  wfrlem11  25540  frrlem5c  25580  fnessref  26364  elunif  27654  stoweidlem27  27743  stoweidlem48  27764  truniALT  28563  truniALTVD  28927  unisnALT  28975
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-v 2950  df-uni 4008
  Copyright terms: Public domain W3C validator