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

Theorem elisset 3455
 Description: An element of a class exists. (Contributed by NM, 1-May-1995.) Reduce dependencies on axioms. (Revised by BJ, 29-Apr-2019.)
Assertion
Ref Expression
elisset (𝐴𝑉 → ∃𝑥 𝑥 = 𝐴)
Distinct variable group:   𝑥,𝐴
Allowed substitution hint:   𝑉(𝑥)

Proof of Theorem elisset
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 exsimpl 1869 . 2 (∃𝑦(𝑦 = 𝐴𝑦𝑉) → ∃𝑦 𝑦 = 𝐴)
2 dfclel 2874 . 2 (𝐴𝑉 ↔ ∃𝑦(𝑦 = 𝐴𝑦𝑉))
3 eqeq1 2805 . . 3 (𝑥 = 𝑦 → (𝑥 = 𝐴𝑦 = 𝐴))
43cbvexvw 2044 . 2 (∃𝑥 𝑥 = 𝐴 ↔ ∃𝑦 𝑦 = 𝐴)
51, 2, 43imtr4i 295 1 (𝐴𝑉 → ∃𝑥 𝑥 = 𝐴)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538  ∃wex 1781   ∈ wcel 2112 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-ext 2773 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2794  df-clel 2873 This theorem is referenced by:  isseti  3458  elex2  3466  elex22  3467  ceqsalt  3477  ceqsalgALT  3480  cgsexg  3487  cgsex2g  3488  cgsex4g  3489  cgsex4gOLD  3490  vtoclgft  3504  vtoclgftOLD  3505  vtoclg1f  3517  vtoclg  3518  vtocleg  3532  vtoclegft  3533  spcimdv  3543  spcegv  3548  spc2egv  3551  spc2ed  3553  eqvincg  3592  iinexg  5211  ralxfr2d  5279  copsex2t  5351  copsex2g  5352  dmopab2rex  5754  fliftf  7051  eloprabga  7244  ovmpt4g  7280  eroveu  8379  mreiincl  16862  metustfbas  23167  brabgaf  30375  bnj852  32301  bnj938  32317  bnj1125  32372  bnj1148  32376  bnj1154  32379  dmopab3rexdif  32760  bj-csbsnlem  34339  bj-snsetex  34394  bj-snglc  34400  copsex2d  34549  prjspeclsp  39593  elex2VD  41531  elex22VD  41532  tpid3gVD  41535  elsprel  43979
 Copyright terms: Public domain W3C validator