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  24478  brabgaf  32586  bnj852  34904  bnj938  34920  bnj1125  34975  bnj1148  34979  bnj1154  34982  fineqvpow  35079  dmopab3rexdif  35385  rexxfr3dALT  35619  bj-isseti  36859  bj-ceqsalt  36867  bj-ceqsalg  36870  bj-spcimdv  36876  bj-csbsnlem  36884  bj-vtoclg1f  36899  bj-snsetex  36944  bj-snglc  36950  bj-clel3gALT  37029  copsex2d  37120  prjspeclsp  42593  elex2VD  44820  elex22VD  44821  tpid3gVD  44824  elsprel  47469