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

Theorem elisset 2798
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 2796 . 2  |-  ( A  e.  V  ->  A  e.  _V )
2 isset 2792 . 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 1528    = wceq 1623    e. wcel 1684   _Vcvv 2788
This theorem is referenced by:  elex22  2799  elex2  2800  ceqsalt  2810  ceqsalg  2812  cgsexg  2819  cgsex2g  2820  cgsex4g  2821  vtoclgft  2834  vtocleg  2854  vtoclegft  2855  spc2egv  2870  spc3egv  2872  tpid3g  3741  iinexg  4171  copsex2t  4253  copsex2g  4254  ralxfr2d  4550  fliftf  5814  eloprabga  5934  ovmpt4g  5970  eroveu  6753  mreiincl  13498  elo  24453  funressnfv  27403  elex2VD  27987  elex22VD  27988  tpid3gVD  27991  bnj852  28326  bnj938  28342  bnj981  28355  bnj1125  28395  bnj1148  28399  bnj1154  28402
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-v 2790
  Copyright terms: Public domain W3C validator