Theorem elisset 2843

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

This theorem is used by:  ceqsalt  3484  ceqsalgALT  3487  cgsexg  3495  cgsex2g  3496  cgsex4g  3497  vtocleg  3517  vtocld  3523  vtoclg1f  3531  spcimdv  3548  spcegv  3552  spc2egv  3554  spc2ed  3556  eqvincg  3602  clel2g  3613  clel4g  3617  elabd2  3624  elabgt  3626  elabgtOLD  3627  ralsng  4636  dfiun2g  4988  nvel  5273  iinexg  5309  ralxfr2d  5372  copsex2t  5464  dmopab2rex  5899  fliftf  7323  eloprabga  7529  ovmpt4g  7567  eroveu  8833  mreiincl  17766  metustfbas  24876  brabgaf  33200  bnj852  35551  bnj938  35567  bnj1125  35622  bnj1148  35626  bnj1154  35629  fineqvpow  35783  dmopab3rexdif  36170  rexxfr3dALT  36404  bj-isseti  37790  bj-ceqsalt  37798  bj-ceqsalg  37801  bj-spcimdv  37807  bj-csbsnlem  37815  bj-vtoclg1f  37830  bj-snsetex  37876  bj-snglc  37882  bj-clel3gALT  37963  cgsex2gd  38058  copsex2d  38060  prjspeclsp  43640  elex2VD  45819  elex22VD  45820  tpid3gVD  45823  elsprel  48556