Theorem elisset 2845

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

Syntax hints:   → wi 4   = wceq 1570  ∃wex 1809   ∈ wcel 2143

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-clel 2838

This theorem is referenced by:  ceqsalt  3488  ceqsalgALT  3491  cgsexg  3499  cgsex2g  3500  cgsex4g  3501  vtocleg  3521  vtocld  3527  vtoclg1f  3535  spcimdv  3552  spcegv  3556  spc2egv  3558  spc2ed  3560  eqvincg  3607  clel2g  3618  clel4g  3622  elabd2  3629  elabgt  3631  elabgtOLD  3632  ralsng  4641  dfiun2g  4994  nvel  5282  iinexg  5318  ralxfr2d  5381  copsex2t  5475  dmopab2rex  5907  fliftf  7313  eloprabga  7519  ovmpt4g  7557  eroveu  8806  mreiincl  17643  metustfbas  24714  brabgaf  32951  bnj852  35309  bnj938  35325  bnj1125  35380  bnj1148  35384  bnj1154  35387  fineqvpow  35528  dmopab3rexdif  35897  rexxfr3dALT  36131  bj-isseti  37533  bj-ceqsalt  37541  bj-ceqsalg  37544  bj-spcimdv  37550  bj-csbsnlem  37558  bj-vtoclg1f  37573  bj-snsetex  37619  bj-snglc  37625  bj-clel3gALT  37704  cgsex2gd  37801  copsex2d  37803  prjspeclsp  43364  elex2VD  45566  elex22VD  45567  tpid3gVD  45570  elsprel  48244