Theorem elisset 2810

Description: An element of a class exists. Use elissetv 2809 instead when sufficient (for instance in usages where 𝑥 is a dummy variable). (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.

Step	Hyp	Ref	Expression
1		elissetv 2809	. 2 ⊢ (𝐴 ∈ 𝑉 → ∃𝑧 𝑧 = 𝐴)
2		iseqsetv-clel 2807	. 2 ⊢ (∃𝑧 𝑧 = 𝐴 ↔ ∃𝑥 𝑥 = 𝐴)
3	1, 2	sylib 218	1 ⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴)

Syntax hints:   → wi 4   = wceq 1540  ∃wex 1779   ∈ wcel 2109

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-clel 2803

This theorem is referenced by:  ceqsalt  3481  ceqsalgALT  3484  cgsexg  3492  cgsex2g  3493  cgsex4g  3494  cgsex4gOLD  3495  vtocleg  3519  vtocld  3527  vtoclg1f  3536  vtoclgOLD  3537  vtoclegftOLD  3555  spcimdv  3559  spcegv  3563  spc2egv  3565  spc2ed  3567  eqvincg  3614  clel2g  3625  clel4g  3629  elabd2  3636  elabgt  3638  elabgtOLD  3639  elabgtOLDOLD  3640  ralsng  4639  dfiun2g  4994  iinexg  5303  ralxfr2d  5365  copsex2t  5452  dmopab2rex  5881  fliftf  7290  eloprabga  7498  ovmpt4g  7536  eroveu  8785  mreiincl  17557  metustfbas  24445  brabgaf  32536  bnj852  34911  bnj938  34927  bnj1125  34982  bnj1148  34986  bnj1154  34989  fineqvpow  35086  dmopab3rexdif  35392  rexxfr3dALT  35626  bj-isseti  36866  bj-ceqsalt  36874  bj-ceqsalg  36877  bj-spcimdv  36883  bj-csbsnlem  36891  bj-vtoclg1f  36906  bj-snsetex  36951  bj-snglc  36957  bj-clel3gALT  37036  copsex2d  37127  prjspeclsp  42600  elex2VD  44827  elex22VD  44828  tpid3gVD  44831  elsprel  47476