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

Theorem elisset 2568
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 2566 . 2  |-  ( A  e.  V  ->  A  e.  _V )
2 isset 2561 . 2  |-  ( A  e.  _V  <->  E. x  x  =  A )
31, 2sylib 127 1  |-  ( A  e.  V  ->  E. x  x  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1243   E.wex 1381    e. wcel 1393   _Vcvv 2557
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-ext 2022
This theorem depends on definitions:  df-bi 110  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-v 2559
This theorem is referenced by:  elex22  2569  elex2  2570  ceqsalt  2580  ceqsalg  2582  cgsexg  2589  cgsex2g  2590  cgsex4g  2591  vtoclgft  2604  vtocleg  2624  vtoclegft  2625  spc2egv  2642  spc2gv  2643  spc3egv  2644  spc3gv  2645  eqvincg  2668  tpid3g  3483  iinexgm  3908  copsex2t  3982  copsex2g  3983  ralxfr2d  4196  rexxfr2d  4197  fliftf  5439  eloprabga  5591  ovmpt4g  5623  eroveu  6197  genpassl  6620  genpassu  6621  nn1suc  7931  bj-inex  10001
  Copyright terms: Public domain W3C validator