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

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

Proof of Theorem elisset
StepHypRef Expression
1 elex 2542 . 2 (A 𝑉A V)
2 isset 2538 . 2 (A V ↔ x x = A)
31, 2sylib 127 1 (A 𝑉x x = A)
Colors of variables: wff set class
Syntax hints:  wi 4  wex 1362   = wceq 1374   wcel 1376  Vcvv 2534
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 1316  ax-gen 1318  ax-ie1 1363  ax-ie2 1364  ax-8 1378  ax-4 1383  ax-17 1402  ax-i9 1406  ax-ial 1411  ax-ext 2005
This theorem depends on definitions:  df-bi 110  df-sb 1629  df-clab 2010  df-cleq 2016  df-clel 2019  df-v 2536
This theorem is referenced by:  elex22  2545  elex2  2546  ceqsalt  2556  ceqsalg  2558  cgsexg  2565  cgsex2g  2566  cgsex4g  2567  vtoclgft  2580  vtocleg  2600  vtoclegft  2601  spc2egv  2618  spc2gv  2619  spc3egv  2620  spc3gv  2621  eqvincg  2644  tpid3g  3435  iinexgm  3861  copsex2t  3935  copsex2g  3936  ralxfr2d  4122  rexxfr2d  4123  fliftf  5341  eloprabga  5493  ovmpt4g  5525  eroveu  6078
  Copyright terms: Public domain W3C validator