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  3478  ceqsalgALT  3481  cgsexg  3489  cgsex2g  3490  cgsex4g  3491  cgsex4gOLD  3492  vtocleg  3516  vtocld  3524  vtoclg1f  3533  vtoclgOLD  3534  vtoclegftOLD  3552  spcimdv  3556  spcegv  3560  spc2egv  3562  spc2ed  3564  eqvincg  3611  clel2g  3622  clel4g  3626  elabd2  3633  elabgt  3635  elabgtOLD  3636  elabgtOLDOLD  3637  ralsng  4635  dfiun2g  4990  iinexg  5298  ralxfr2d  5360  copsex2t  5447  dmopab2rex  5871  fliftf  7272  eloprabga  7478  ovmpt4g  7516  eroveu  8762  mreiincl  17533  metustfbas  24421  brabgaf  32509  bnj852  34884  bnj938  34900  bnj1125  34955  bnj1148  34959  bnj1154  34962  fineqvpow  35059  dmopab3rexdif  35365  rexxfr3dALT  35599  bj-isseti  36839  bj-ceqsalt  36847  bj-ceqsalg  36850  bj-spcimdv  36856  bj-csbsnlem  36864  bj-vtoclg1f  36879  bj-snsetex  36924  bj-snglc  36930  bj-clel3gALT  37009  copsex2d  37100  prjspeclsp  42573  elex2VD  44800  elex22VD  44801  tpid3gVD  44804  elsprel  47449