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  3470  ceqsalgALT  3473  cgsexg  3481  cgsex2g  3482  cgsex4g  3483  cgsex4gOLD  3484  vtocleg  3508  vtocld  3516  vtoclg1f  3525  vtoclgOLD  3526  vtoclegftOLD  3544  spcimdv  3548  spcegv  3552  spc2egv  3554  spc2ed  3556  eqvincg  3603  clel2g  3614  clel4g  3618  elabd2  3625  elabgt  3627  elabgtOLD  3628  elabgtOLDOLD  3629  ralsng  4627  dfiun2g  4980  iinexg  5287  ralxfr2d  5349  copsex2t  5435  dmopab2rex  5860  fliftf  7252  eloprabga  7458  ovmpt4g  7496  eroveu  8739  mreiincl  17498  metustfbas  24443  brabgaf  32553  bnj852  34888  bnj938  34904  bnj1125  34959  bnj1148  34963  bnj1154  34966  fineqvpow  35071  dmopab3rexdif  35382  rexxfr3dALT  35616  bj-isseti  36856  bj-ceqsalt  36864  bj-ceqsalg  36867  bj-spcimdv  36873  bj-csbsnlem  36881  bj-vtoclg1f  36896  bj-snsetex  36941  bj-snglc  36947  bj-clel3gALT  37026  copsex2d  37117  prjspeclsp  42589  elex2VD  44815  elex22VD  44816  tpid3gVD  44819  elsprel  47463