Theorem elisset 2818

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

Syntax hints:   → wi 4   = wceq 1541  ∃wex 1780   ∈ wcel 2113

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-clel 2811

This theorem is referenced by:  ceqsalt  3474  ceqsalgALT  3477  cgsexg  3485  cgsex2g  3486  cgsex4g  3487  cgsex4gOLD  3488  vtocleg  3510  vtocld  3518  vtoclg1f  3526  spcimdv  3547  spcegv  3551  spc2egv  3553  spc2ed  3555  eqvincg  3602  clel2g  3613  clel4g  3617  elabd2  3624  elabgt  3626  elabgtOLD  3627  elabgtOLDOLD  3628  ralsng  4632  dfiun2g  4985  iinexg  5293  ralxfr2d  5355  copsex2t  5440  dmopab2rex  5866  fliftf  7261  eloprabga  7467  ovmpt4g  7505  eroveu  8749  mreiincl  17515  metustfbas  24501  brabgaf  32684  bnj852  35077  bnj938  35093  bnj1125  35148  bnj1148  35152  bnj1154  35155  fineqvpow  35271  dmopab3rexdif  35599  rexxfr3dALT  35833  bj-isseti  37079  bj-ceqsalt  37087  bj-ceqsalg  37090  bj-spcimdv  37096  bj-csbsnlem  37104  bj-vtoclg1f  37119  bj-snsetex  37164  bj-snglc  37170  bj-clel3gALT  37249  copsex2d  37344  prjspeclsp  42865  elex2VD  45088  elex22VD  45089  tpid3gVD  45092  elsprel  47731