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

Theorem elisset 3503
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 1860 . 2 (∃𝑦(𝑦 = 𝐴𝑦𝑉) → ∃𝑦 𝑦 = 𝐴)
2 dfclel 2891 . 2 (𝐴𝑉 ↔ ∃𝑦(𝑦 = 𝐴𝑦𝑉))
3 eqeq1 2822 . . 3 (𝑥 = 𝑦 → (𝑥 = 𝐴𝑦 = 𝐴))
43cbvexvw 2035 . 2 (∃𝑥 𝑥 = 𝐴 ↔ ∃𝑦 𝑦 = 𝐴)
51, 2, 43imtr4i 293 1 (𝐴𝑉 → ∃𝑥 𝑥 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1528  wex 1771  wcel 2105
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-cleq 2811  df-clel 2890
This theorem is referenced by:  isseti  3506  elex2  3514  elex22  3515  ceqsalt  3525  ceqsalgALT  3528  cgsexg  3535  cgsex2g  3536  cgsex4g  3537  vtoclgft  3551  vtoclgftOLD  3552  vtoclg1f  3564  vtocleg  3578  vtoclegft  3579  spcimdv  3589  spcegv  3594  spc2egv  3597  spc2ed  3599  eqvincg  3638  iinexg  5235  ralxfr2d  5301  copsex2t  5374  copsex2g  5375  dmopab2rex  5779  fliftf  7057  eloprabga  7250  ovmpt4g  7286  eroveu  8381  mreiincl  16855  metustfbas  23094  brabgaf  30287  bnj852  32092  bnj938  32108  bnj1125  32161  bnj1148  32165  bnj1154  32168  dmopab3rexdif  32549  bj-csbsnlem  34117  bj-snsetex  34172  bj-snglc  34178  copsex2d  34323  prjspeclsp  39140  elex2VD  41049  elex22VD  41050  tpid3gVD  41053  elsprel  43514
  Copyright terms: Public domain W3C validator