ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  elisset Unicode version

Theorem elisset 2674
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 2671 . 2  |-  ( A  e.  V  ->  A  e.  _V )
2 isset 2666 . 2  |-  ( A  e.  _V  <->  E. x  x  =  A )
31, 2sylib 121 1  |-  ( A  e.  V  ->  E. x  x  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1316   E.wex 1453    e. wcel 1465   _Vcvv 2660
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1408  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-4 1472  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-sb 1721  df-clab 2104  df-cleq 2110  df-clel 2113  df-v 2662
This theorem is referenced by:  elex22  2675  elex2  2676  ceqsalt  2686  ceqsalg  2688  cgsexg  2695  cgsex2g  2696  cgsex4g  2697  vtoclgft  2710  vtocleg  2731  vtoclegft  2732  spc2egv  2749  spc2gv  2750  spc3egv  2751  spc3gv  2752  eqvincg  2783  tpid3g  3608  iinexgm  4049  copsex2t  4137  copsex2g  4138  ralxfr2d  4355  rexxfr2d  4356  fliftf  5668  eloprabga  5826  ovmpt4g  5861  spc2ed  6098  eroveu  6488  supelti  6857  genpassl  7300  genpassu  7301  eqord1  8213  nn1suc  8703  bj-inex  13001
  Copyright terms: Public domain W3C validator