Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  elisset Structured version   Visualization version   GIF version

Theorem elisset 3188
 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 3185 . 2 (𝐴𝑉𝐴 ∈ V)
2 isset 3180 . 2 (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
31, 2sylib 207 1 (𝐴𝑉 → ∃𝑥 𝑥 = 𝐴)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1475  ∃wex 1695   ∈ wcel 1977  Vcvv 3173 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-12 2034  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-an 385  df-tru 1478  df-ex 1696  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-v 3175 This theorem is referenced by:  elex2  3189  elex22  3190  ceqsalt  3201  ceqsalgALT  3204  cgsexg  3211  cgsex2g  3212  cgsex4g  3213  vtoclgft  3227  vtoclgftOLD  3228  vtocleg  3252  vtoclegft  3253  spc2egv  3268  spc3egv  3270  tpid3gOLD  4249  iinexg  4751  ralxfr2d  4808  copsex2t  4883  copsex2g  4884  fliftf  6465  eloprabga  6645  ovmpt4g  6681  eroveu  7729  mreiincl  16079  metustfbas  22172  spc2ed  28696  eqvincg  28698  brabgaf  28800  bnj852  30245  bnj938  30261  bnj1125  30314  bnj1148  30318  bnj1154  30321  bj-csbsnlem  32090  bj-snsetex  32144  bj-snglc  32150  elex2VD  38095  elex22VD  38096  tpid3gVD  38099
 Copyright terms: Public domain W3C validator