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

Theorem elisset 2926
Description: An element of a class exists. (Contributed by NM, 1-May-1995.)
Assertion
Ref Expression
elisset  |-  ( A  e.  V  ->  E. x  x  =  A )
Distinct variable group:    x, A
Allowed substitution hint:    V( x)

Proof of Theorem elisset
StepHypRef Expression
1 elex 2924 . 2  |-  ( A  e.  V  ->  A  e.  _V )
2 isset 2920 . 2  |-  ( A  e.  _V  <->  E. x  x  =  A )
31, 2sylib 189 1  |-  ( A  e.  V  ->  E. x  x  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4   E.wex 1547    = wceq 1649    e. wcel 1721   _Vcvv 2916
This theorem is referenced by:  elex22  2927  elex2  2928  ceqsalt  2938  ceqsalg  2940  cgsexg  2947  cgsex2g  2948  cgsex4g  2949  vtoclgft  2962  vtocleg  2982  vtoclegft  2983  spc2egv  2998  spc3egv  3000  tpid3g  3879  iinexg  4320  copsex2t  4403  copsex2g  4404  ralxfr2d  4698  fliftf  5996  eloprabga  6119  ovmpt4g  6155  eroveu  6958  mreiincl  13776  metustfbasOLD  18548  metustfbas  18549  eqvincg  23914  elex2VD  28659  elex22VD  28660  tpid3gVD  28663  bnj852  28998  bnj938  29014  bnj981  29027  bnj1125  29067  bnj1148  29071  bnj1154  29074
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-11 1757  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-v 2918
  Copyright terms: Public domain W3C validator