Theorem elisset 2816

Description: An element of a class exists. Use elissetv 2815 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 2815	. 2 ⊢ (𝐴 ∈ 𝑉 → ∃𝑧 𝑧 = 𝐴)
2		iseqsetv-clel 2813	. 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 2713  df-clel 2809

This theorem is referenced by:  ceqsalt  3472  ceqsalgALT  3475  cgsexg  3483  cgsex2g  3484  cgsex4g  3485  cgsex4gOLD  3486  vtocleg  3508  vtocld  3516  vtoclg1f  3524  spcimdv  3545  spcegv  3549  spc2egv  3551  spc2ed  3553  eqvincg  3600  clel2g  3611  clel4g  3615  elabd2  3622  elabgt  3624  elabgtOLD  3625  elabgtOLDOLD  3626  ralsng  4630  dfiun2g  4983  iinexg  5291  ralxfr2d  5353  copsex2t  5438  dmopab2rex  5864  fliftf  7259  eloprabga  7465  ovmpt4g  7503  eroveu  8747  mreiincl  17513  metustfbas  24499  brabgaf  32633  bnj852  35026  bnj938  35042  bnj1125  35097  bnj1148  35101  bnj1154  35104  fineqvpow  35220  dmopab3rexdif  35548  rexxfr3dALT  35782  bj-isseti  37022  bj-ceqsalt  37030  bj-ceqsalg  37033  bj-spcimdv  37039  bj-csbsnlem  37047  bj-vtoclg1f  37062  bj-snsetex  37107  bj-snglc  37113  bj-clel3gALT  37192  copsex2d  37283  prjspeclsp  42797  elex2VD  45020  elex22VD  45021  tpid3gVD  45024  elsprel  47663