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

Theorem elisset 3213
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 3210 . 2 (𝐴𝑉𝐴 ∈ V)
2 isset 3205 . 2 (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
31, 2sylib 208 1 (𝐴𝑉 → ∃𝑥 𝑥 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1482  wex 1703  wcel 1989  Vcvv 3198
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-9 1998  ax-12 2046  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-an 386  df-tru 1485  df-ex 1704  df-sb 1880  df-clab 2608  df-cleq 2614  df-clel 2617  df-v 3200
This theorem is referenced by:  elex2  3214  elex22  3215  ceqsalt  3226  ceqsalgALT  3229  cgsexg  3236  cgsex2g  3237  cgsex4g  3238  vtoclgft  3252  vtoclgftOLD  3253  vtocleg  3277  vtoclegft  3278  spc2egv  3293  spc3egv  3295  eqvincg  3327  tpid3gOLD  4304  iinexg  4822  ralxfr2d  4880  copsex2t  4955  copsex2g  4956  fliftf  6562  eloprabga  6744  ovmpt4g  6780  eroveu  7839  mreiincl  16250  metustfbas  22356  spc2ed  29296  brabgaf  29404  bnj852  30976  bnj938  30992  bnj1125  31045  bnj1148  31049  bnj1154  31052  bj-csbsnlem  32882  bj-snsetex  32935  bj-snglc  32941  elex2VD  38899  elex22VD  38900  tpid3gVD  38903  elsprel  41496
  Copyright terms: Public domain W3C validator