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

Theorem elisset 2910
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 2908 . 2  |-  ( A  e.  V  ->  A  e.  _V )
2 isset 2904 . 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 1717   _Vcvv 2900
This theorem is referenced by:  elex22  2911  elex2  2912  ceqsalt  2922  ceqsalg  2924  cgsexg  2931  cgsex2g  2932  cgsex4g  2933  vtoclgft  2946  vtocleg  2966  vtoclegft  2967  spc2egv  2982  spc3egv  2984  tpid3g  3863  iinexg  4302  copsex2t  4385  copsex2g  4386  ralxfr2d  4680  fliftf  5977  eloprabga  6100  ovmpt4g  6136  eroveu  6936  mreiincl  13749  metustfbas  18478  eqvincg  23806  elex2VD  28292  elex22VD  28293  tpid3gVD  28296  bnj852  28631  bnj938  28647  bnj981  28660  bnj1125  28700  bnj1148  28704  bnj1154  28707
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 1661  ax-8 1682  ax-11 1753  ax-ext 2369
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-sb 1656  df-clab 2375  df-cleq 2381  df-clel 2384  df-v 2902
  Copyright terms: Public domain W3C validator