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

Theorem elisset 3364
 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 3361 . 2 (𝐴𝑉𝐴 ∈ V)
2 isset 3356 . 2 (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
31, 2sylib 208 1 (𝐴𝑉 → ∃𝑥 𝑥 = 𝐴)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1630  ∃wex 1851   ∈ wcel 2144  Vcvv 3349 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-9 2153  ax-12 2202  ax-ext 2750 This theorem depends on definitions:  df-bi 197  df-an 383  df-tru 1633  df-ex 1852  df-sb 2049  df-clab 2757  df-cleq 2763  df-clel 2766  df-v 3351 This theorem is referenced by:  elex2  3365  elex22  3366  ceqsalt  3377  ceqsalgALT  3380  cgsexg  3387  cgsex2g  3388  cgsex4g  3389  vtoclgft  3403  vtoclgftOLD  3404  vtocleg  3428  vtoclegft  3429  spc2egv  3444  spc3egv  3446  eqvincg  3477  iinexg  4952  ralxfr2d  5010  copsex2t  5084  copsex2g  5085  fliftf  6707  eloprabga  6893  ovmpt4g  6929  eroveu  7994  mreiincl  16463  metustfbas  22581  spc2ed  29646  brabgaf  29752  bnj852  31323  bnj938  31339  bnj1125  31392  bnj1148  31396  bnj1154  31399  bj-csbsnlem  33221  bj-snsetex  33276  bj-snglc  33282  elex2VD  39589  elex22VD  39590  tpid3gVD  39593  elsprel  42243
 Copyright terms: Public domain W3C validator