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

Theorem elisset 2811
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 2809 . 2  |-  ( A  e.  V  ->  A  e.  _V )
2 isset 2805 . 2  |-  ( A  e.  _V  <->  E. x  x  =  A )
31, 2sylib 188 1  |-  ( A  e.  V  ->  E. x  x  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4   E.wex 1531    = wceq 1632    e. wcel 1696   _Vcvv 2801
This theorem is referenced by:  elex22  2812  elex2  2813  ceqsalt  2823  ceqsalg  2825  cgsexg  2832  cgsex2g  2833  cgsex4g  2834  vtoclgft  2847  vtocleg  2867  vtoclegft  2868  spc2egv  2883  spc3egv  2885  tpid3g  3754  iinexg  4187  copsex2t  4269  copsex2g  4270  ralxfr2d  4566  fliftf  5830  eloprabga  5950  ovmpt4g  5986  eroveu  6769  mreiincl  13514  eqvincg  23146  elo  25144  funressnfv  28096  elex2VD  28930  elex22VD  28931  tpid3gVD  28934  bnj852  29269  bnj938  29285  bnj981  29298  bnj1125  29338  bnj1148  29342  bnj1154  29345
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-11 1727  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1532  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-v 2803
  Copyright terms: Public domain W3C validator