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

Theorem elisset 2671
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 2668 . 2 (𝐴𝑉𝐴 ∈ V)
2 isset 2663 . 2 (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
31, 2sylib 121 1 (𝐴𝑉 → ∃𝑥 𝑥 = 𝐴)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1314  wex 1451  wcel 1463  Vcvv 2657
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1406  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-ext 2097
This theorem depends on definitions:  df-bi 116  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111  df-v 2659
This theorem is referenced by:  elex22  2672  elex2  2673  ceqsalt  2683  ceqsalg  2685  cgsexg  2692  cgsex2g  2693  cgsex4g  2694  vtoclgft  2707  vtocleg  2728  vtoclegft  2729  spc2egv  2746  spc2gv  2747  spc3egv  2748  spc3gv  2749  eqvincg  2779  tpid3g  3604  iinexgm  4039  copsex2t  4127  copsex2g  4128  ralxfr2d  4345  rexxfr2d  4346  fliftf  5654  eloprabga  5812  ovmpt4g  5847  spc2ed  6084  eroveu  6474  supelti  6841  genpassl  7280  genpassu  7281  eqord1  8164  nn1suc  8649  bj-inex  12797
  Copyright terms: Public domain W3C validator