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

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

Proof of Theorem elisset
StepHypRef Expression
1 elex 2867 . 2
2 isset 2863 . 2
31, 2sylib 188 1
Colors of variables: wff setvar class
Syntax hints:   wi 4  wex 1541   wceq 1642   wcel 1710  cvv 2859
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 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