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

Theorem elisset 3433
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 3430 . 2 (𝐴𝑉𝐴 ∈ V)
2 isset 3425 . 2 (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
31, 2sylib 210 1 (𝐴𝑉 → ∃𝑥 𝑥 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1658  wex 1880  wcel 2166  Vcvv 3415
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-12 2222  ax-ext 2804
This theorem depends on definitions:  df-bi 199  df-an 387  df-tru 1662  df-ex 1881  df-sb 2070  df-clab 2813  df-cleq 2819  df-clel 2822  df-v 3417
This theorem is referenced by:  elex2  3434  elex22  3435  ceqsalt  3446  ceqsalgALT  3449  cgsexg  3456  cgsex2g  3457  cgsex4g  3458  vtoclgft  3472  vtocleg  3497  vtoclegft  3498  spc2egv  3513  spc3egv  3515  eqvincg  3548  iinexg  5047  ralxfr2d  5111  copsex2t  5178  copsex2g  5179  fliftf  6821  eloprabga  7008  ovmpt4g  7044  eroveu  8109  mreiincl  16610  metustfbas  22733  spc2ed  29868  brabgaf  29968  bnj852  31538  bnj938  31554  bnj1125  31607  bnj1148  31611  bnj1154  31614  bj-csbsnlem  33420  bj-snsetex  33474  bj-snglc  33480  elex2VD  39893  elex22VD  39894  tpid3gVD  39897  elsprel  42573
  Copyright terms: Public domain W3C validator