Theorem elisset 2842

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

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

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 1943  ax-6 2000  ax-7 2041  ax-8 2147

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-clel 2835

This theorem is used by:  ceqsalt  3483  ceqsalgALT  3486  cgsexg  3494  cgsex2g  3495  cgsex4g  3496  vtocleg  3516  vtocld  3522  vtoclg1f  3530  spcimdv  3547  spcegv  3551  spc2egv  3553  spc2ed  3555  eqvincg  3602  clel2g  3613  clel4g  3617  elabd2  3624  elabgt  3626  elabgtOLD  3627  ralsng  4636  dfiun2g  4988  nvel  5276  iinexg  5312  ralxfr2d  5375  copsex2t  5469  dmopab2rex  5901  fliftf  7317  eloprabga  7523  ovmpt4g  7561  eroveu  8813  mreiincl  17681  metustfbas  24784  brabgaf  33080  bnj852  35431  bnj938  35447  bnj1125  35502  bnj1148  35506  bnj1154  35509  fineqvpow  35642  dmopab3rexdif  35985  rexxfr3dALT  36219  bj-isseti  37622  bj-ceqsalt  37630  bj-ceqsalg  37633  bj-spcimdv  37639  bj-csbsnlem  37647  bj-vtoclg1f  37662  bj-snsetex  37708  bj-snglc  37714  bj-clel3gALT  37793  cgsex2gd  37890  copsex2d  37892  prjspeclsp  43459  elex2VD  45661  elex22VD  45662  tpid3gVD  45665  elsprel  48376