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

Theorem elisset 2958
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 2956 . 2  |-  ( A  e.  V  ->  A  e.  _V )
2 isset 2952 . 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 1550    = wceq 1652    e. wcel 1725   _Vcvv 2948
This theorem is referenced by:  elex22  2959  elex2  2960  ceqsalt  2970  ceqsalg  2972  cgsexg  2979  cgsex2g  2980  cgsex4g  2981  vtoclgft  2994  vtocleg  3014  vtoclegft  3015  spc2egv  3030  spc3egv  3032  tpid3g  3911  iinexg  4352  copsex2t  4435  copsex2g  4436  ralxfr2d  4731  fliftf  6029  eloprabga  6152  ovmpt4g  6188  eroveu  6991  mreiincl  13813  metustfbasOLD  18587  metustfbas  18588  eqvincg  23953  elex2VD  28887  elex22VD  28888  tpid3gVD  28891  bnj852  29229  bnj938  29245  bnj981  29258  bnj1125  29298  bnj1148  29302  bnj1154  29305
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-v 2950
  Copyright terms: Public domain W3C validator