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

Theorem elisset 2585
 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 2583 . 2 (𝐴𝑉𝐴 ∈ V)
2 isset 2578 . 2 (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
31, 2sylib 131 1 (𝐴𝑉 → ∃𝑥 𝑥 = 𝐴)
 Colors of variables: wff set class Syntax hints:   → wi 4   = wceq 1259  ∃wex 1397   ∈ wcel 1409  Vcvv 2574 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-4 1416  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-ext 2038 This theorem depends on definitions:  df-bi 114  df-sb 1662  df-clab 2043  df-cleq 2049  df-clel 2052  df-v 2576 This theorem is referenced by:  elex22  2586  elex2  2587  ceqsalt  2597  ceqsalg  2599  cgsexg  2606  cgsex2g  2607  cgsex4g  2608  vtoclgft  2621  vtocleg  2641  vtoclegft  2642  spc2egv  2659  spc2gv  2660  spc3egv  2661  spc3gv  2662  eqvincg  2690  tpid3g  3510  iinexgm  3935  copsex2t  4009  copsex2g  4010  ralxfr2d  4223  rexxfr2d  4224  fliftf  5466  eloprabga  5618  ovmpt4g  5650  spc2ed  5881  eroveu  6227  genpassl  6679  genpassu  6680  nn1suc  8008  bj-inex  10393
 Copyright terms: Public domain W3C validator