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

Theorem eluni 3846
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 2809 . 2  |-  ( A  e.  U. B  ->  A  e.  _V )
2 elex 2809 . . . 4  |-  ( A  e.  x  ->  A  e.  _V )
32adantr 451 . . 3  |-  ( ( A  e.  x  /\  x  e.  B )  ->  A  e.  _V )
43exlimiv 1624 . 2  |-  ( E. x ( A  e.  x  /\  x  e.  B )  ->  A  e.  _V )
5 eleq1 2356 . . . . 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 1616 . . 3  |-  ( y  =  A  ->  ( E. x ( y  e.  x  /\  x  e.  B )  <->  E. x
( A  e.  x  /\  x  e.  B
) ) )
8 df-uni 3844 . . 3  |-  U. B  =  { y  |  E. x ( y  e.  x  /\  x  e.  B ) }
97, 8elab2g 2929 . 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 1531    = wceq 1632    e. wcel 1696   _Vcvv 2801   U.cuni 3843
This theorem is referenced by:  eluni2  3847  elunii  3848  eluniab  3855  uniun  3862  uniin  3863  uniss  3864  unissb  3873  dftr2  4131  unipw  4240  uniex2  4531  uniuni  4543  dmuni  4904  fununi  5332  elunirnALT  5795  tfrlem7  6415  tfrlem9a  6418  inf2  7340  inf3lem2  7346  rankwflemb  7481  cardprclem  7628  carduni  7630  iunfictbso  7757  kmlem3  7794  kmlem4  7795  cfub  7891  isf34lem4  8019  grothtsk  8473  suplem1pr  8692  isbasis2g  16702  tgval2  16710  ntreq0  16830  cmpsublem  17142  cmpsub  17143  cmpcld  17145  is1stc2  17184  alexsubALTlem3  17759  alexsubALT  17761  wfrlem11  24337  frrlem5c  24358  fnessref  26396  elunif  27790  stoweidlem27  27879  stoweidlem48  27900  mpt2xopxnop0  28197  truniALT  28604  truniALTVD  28970  unisnALT  29018
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-uni 3844
  Copyright terms: Public domain W3C validator