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  3464  ceqsalgALT  3467  cgsexg  3475  cgsex2g  3476  cgsex4g  3477  vtocleg  3499  vtocld  3507  vtoclg1f  3515  spcimdv  3536  spcegv  3540  spc2egv  3542  spc2ed  3544  eqvincg  3591  clel2g  3602  clel4g  3606  elabd2  3613  elabgt  3615  elabgtOLD  3616  elabgtOLDOLD  3617  ralsng  4620  dfiun2g  4973  iinexg  5286  ralxfr2d  5348  copsex2t  5441  dmopab2rex  5867  fliftf  7264  eloprabga  7470  ovmpt4g  7508  eroveu  8753  mreiincl  17552  metustfbas  24535  brabgaf  32697  bnj852  35082  bnj938  35098  bnj1125  35153  bnj1148  35157  bnj1154  35160  fineqvpow  35278  dmopab3rexdif  35606  rexxfr3dALT  35840  bj-isseti  37204  bj-ceqsalt  37212  bj-ceqsalg  37215  bj-spcimdv  37221  bj-csbsnlem  37229  bj-vtoclg1f  37244  bj-snsetex  37289  bj-snglc  37295  bj-clel3gALT  37374  cgsex2gd  37470  copsex2d  37472  prjspeclsp  43062  elex2VD  45285  elex22VD  45286  tpid3gVD  45289  elsprel  47950