Theorem elisset 2813

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

Syntax hints:   → wi 4   = wceq 1541  ∃wex 1780   ∈ wcel 2111

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 2113

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-clel 2806

This theorem is referenced by:  ceqsalt  3470  ceqsalgALT  3473  cgsexg  3481  cgsex2g  3482  cgsex4g  3483  cgsex4gOLD  3484  vtocleg  3506  vtocld  3514  vtoclg1f  3522  spcimdv  3543  spcegv  3547  spc2egv  3549  spc2ed  3551  eqvincg  3598  clel2g  3609  clel4g  3613  elabd2  3620  elabgt  3622  elabgtOLD  3623  elabgtOLDOLD  3624  ralsng  4625  dfiun2g  4978  iinexg  5284  ralxfr2d  5346  copsex2t  5430  dmopab2rex  5856  fliftf  7249  eloprabga  7455  ovmpt4g  7493  eroveu  8736  mreiincl  17498  metustfbas  24472  brabgaf  32589  bnj852  34933  bnj938  34949  bnj1125  35004  bnj1148  35008  bnj1154  35011  fineqvpow  35138  dmopab3rexdif  35449  rexxfr3dALT  35683  bj-isseti  36922  bj-ceqsalt  36930  bj-ceqsalg  36933  bj-spcimdv  36939  bj-csbsnlem  36947  bj-vtoclg1f  36962  bj-snsetex  37007  bj-snglc  37013  bj-clel3gALT  37092  copsex2d  37183  prjspeclsp  42715  elex2VD  44940  elex22VD  44941  tpid3gVD  44944  elsprel  47585