Theorem elisset 2846

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  ∃wex 1812   ∈ wcel 2147

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-clel 2839

This theorem is used by:  ceqsalt  3487  ceqsalgALT  3490  cgsexg  3498  cgsex2g  3499  cgsex4g  3500  vtocleg  3520  vtocld  3526  vtoclg1f  3534  spcimdv  3551  spcegv  3555  spc2egv  3557  spc2ed  3559  eqvincg  3605  clel2g  3616  clel4g  3620  elabd2  3627  elabgt  3629  elabgtOLD  3630  ralsng  4637  dfiun2g  4993  nvel  5279  iinexg  5316  ralxfr2d  5379  copsex2t  5471  dmopab2rex  5911  fliftf  7354  eloprabga  7560  ovmpt4g  7599  eroveu  8871  mreiincl  17816  metustfbas  24931  brabgaf  33298  bnj852  35662  bnj938  35678  bnj1125  35733  bnj1148  35737  bnj1154  35740  fineqvpow  35924  dmopab3rexdif  36378  rexxfr3dALT  36612  bj-isseti  38005  bj-ceqsalt  38013  bj-ceqsalg  38016  bj-spcimdv  38022  bj-csbsnlem  38030  bj-vtoclg1f  38045  bj-snsetex  38091  bj-snglc  38097  bj-clel3gALT  38233  cgsex2gd  38329  copsex2d  38331  prjspeclsp  43906  elex2VD  46080  elex22VD  46081  tpid3gVD  46084  elsprel  48830