Theorem elisset 2819

Description: An element of a class exists. Use elissetv 2818 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 2818	. 2 ⊢ (𝐴 ∈ 𝑉 → ∃𝑧 𝑧 = 𝐴)
2		iseqsetv-clel 2816	. 2 ⊢ (∃𝑧 𝑧 = 𝐴 ↔ ∃𝑥 𝑥 = 𝐴)
3	1, 2	sylib 218	1 ⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴)

Syntax hints:   → wi 4   = wceq 1542  ∃wex 1781   ∈ wcel 2114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-clel 2812

This theorem is referenced by:  ceqsalt  3476  ceqsalgALT  3479  cgsexg  3487  cgsex2g  3488  cgsex4g  3489  cgsex4gOLD  3490  vtocleg  3512  vtocld  3520  vtoclg1f  3528  spcimdv  3549  spcegv  3553  spc2egv  3555  spc2ed  3557  eqvincg  3604  clel2g  3615  clel4g  3619  elabd2  3626  elabgt  3628  elabgtOLD  3629  elabgtOLDOLD  3630  ralsng  4634  dfiun2g  4987  iinexg  5295  ralxfr2d  5357  copsex2t  5448  dmopab2rex  5874  fliftf  7271  eloprabga  7477  ovmpt4g  7515  eroveu  8761  mreiincl  17527  metustfbas  24513  brabgaf  32696  bnj852  35097  bnj938  35113  bnj1125  35168  bnj1148  35172  bnj1154  35175  fineqvpow  35293  dmopab3rexdif  35621  rexxfr3dALT  35855  bj-isseti  37126  bj-ceqsalt  37134  bj-ceqsalg  37137  bj-spcimdv  37143  bj-csbsnlem  37151  bj-vtoclg1f  37166  bj-snsetex  37211  bj-snglc  37217  bj-clel3gALT  37296  cgsex2gd  37392  copsex2d  37394  prjspeclsp  42970  elex2VD  45193  elex22VD  45194  tpid3gVD  45197  elsprel  47835