New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  elisset GIF version

Theorem elisset 2869
 Description: An element of a class exists. (Contributed by NM, 1-May-1995.)
Assertion
Ref Expression
elisset (A Vx x = A)
Distinct variable group:   x,A
Allowed substitution hint:   V(x)

Proof of Theorem elisset
StepHypRef Expression
1 elex 2867 . 2 (A VA V)
2 isset 2863 . 2 (A V ↔ x x = A)
31, 2sylib 188 1 (A Vx x = A)
 Colors of variables: wff setvar class Syntax hints:   → wi 4  ∃wex 1541   = wceq 1642   ∈ wcel 1710  Vcvv 2859 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746  ax-ext 2334 This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1542  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-v 2861 This theorem is referenced by:  elex22  2870  elex2  2871  ceqsalt  2881  ceqsalg  2883  cgsexg  2890  cgsex2g  2891  cgsex4g  2892  vtoclgft  2905  vtocleg  2925  vtoclegft  2926  spc2egv  2941  spc3egv  2943  tpid3g  3831  opkelcokg  4261  copsex2t  4608  copsex2g  4609  ovmpt4g  5710  ncelncs  6120
 Copyright terms: Public domain W3C validator