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

Theorem eluni 3830
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 2796 . 2  |-  ( A  e.  U. B  ->  A  e.  _V )
2 elex 2796 . . . 4  |-  ( A  e.  x  ->  A  e.  _V )
32adantr 451 . . 3  |-  ( ( A  e.  x  /\  x  e.  B )  ->  A  e.  _V )
43exlimiv 1666 . 2  |-  ( E. x ( A  e.  x  /\  x  e.  B )  ->  A  e.  _V )
5 eleq1 2343 . . . . 5  |-  ( y  =  A  ->  (
y  e.  x  <->  A  e.  x ) )
65anbi1d 685 . . . 4  |-  ( y  =  A  ->  (
( y  e.  x  /\  x  e.  B
)  <->  ( A  e.  x  /\  x  e.  B ) ) )
76exbidv 1612 . . 3  |-  ( y  =  A  ->  ( E. x ( y  e.  x  /\  x  e.  B )  <->  E. x
( A  e.  x  /\  x  e.  B
) ) )
8 df-uni 3828 . . 3  |-  U. B  =  { y  |  E. x ( y  e.  x  /\  x  e.  B ) }
97, 8elab2g 2916 . 2  |-  ( A  e.  _V  ->  ( A  e.  U. B  <->  E. x
( A  e.  x  /\  x  e.  B
) ) )
101, 4, 9pm5.21nii 342 1  |-  ( A  e.  U. B  <->  E. x
( A  e.  x  /\  x  e.  B
) )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    /\ wa 358   E.wex 1528    = wceq 1623    e. wcel 1684   _Vcvv 2788   U.cuni 3827
This theorem is referenced by:  eluni2  3831  elunii  3832  eluniab  3839  uniun  3846  uniin  3847  uniss  3848  unissb  3857  dftr2  4115  unipw  4224  uniex2  4515  uniuni  4527  dmuni  4888  fununi  5316  elunirnALT  5779  tfrlem7  6399  tfrlem9a  6402  inf2  7324  inf3lem2  7330  rankwflemb  7465  cardprclem  7612  carduni  7614  iunfictbso  7741  kmlem3  7778  kmlem4  7779  cfub  7875  isf34lem4  8003  grothtsk  8457  suplem1pr  8676  isbasis2g  16686  tgval2  16694  ntreq0  16814  cmpsublem  17126  cmpsub  17127  cmpcld  17129  is1stc2  17168  alexsubALTlem3  17743  alexsubALT  17745  wfrlem11  23677  frrlem5c  23698  fnessref  25705  elunif  27099  stoweidlem27  27188  stoweidlem48  27209  truniALT  27678  truniALTVD  28027  unisnALT  28075
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