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

Theorem elisset 2624
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 2621 . 2 (𝐴𝑉𝐴 ∈ V)
2 isset 2616 . 2 (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
31, 2sylib 120 1 (𝐴𝑉 → ∃𝑥 𝑥 = 𝐴)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1285  wex 1422  wcel 1434  Vcvv 2612
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-ext 2065
This theorem depends on definitions:  df-bi 115  df-sb 1688  df-clab 2070  df-cleq 2076  df-clel 2079  df-v 2614
This theorem is referenced by:  elex22  2625  elex2  2626  ceqsalt  2636  ceqsalg  2638  cgsexg  2645  cgsex2g  2646  cgsex4g  2647  vtoclgft  2660  vtocleg  2680  vtoclegft  2681  spc2egv  2698  spc2gv  2699  spc3egv  2700  spc3gv  2701  eqvincg  2729  tpid3g  3529  iinexgm  3955  copsex2t  4036  copsex2g  4037  ralxfr2d  4250  rexxfr2d  4251  fliftf  5518  eloprabga  5670  ovmpt4g  5702  spc2ed  5933  eroveu  6313  supelti  6604  genpassl  6986  genpassu  6987  nn1suc  8335  bj-inex  11141
  Copyright terms: Public domain W3C validator