Theorem elisset 2844

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

Syntax hints:   → wi 4   = wceq 1560  ∃wex 1799   ∈ wcel 2142

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-clel 2837

This theorem is referenced by:  ceqsalt  3487  ceqsalgALT  3490  cgsexg  3498  cgsex2g  3499  cgsex4g  3500  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  4634  dfiun2g  4987  nvel  5269  iinexg  5304  ralxfr2d  5367  copsex2t  5461  dmopab2rex  5893  fliftf  7299  eloprabga  7505  ovmpt4g  7543  eroveu  8794  mreiincl  17624  metustfbas  24617  brabgaf  32808  bnj852  35216  bnj938  35232  bnj1125  35287  bnj1148  35291  bnj1154  35294  fineqvpow  35411  dmopab3rexdif  35755  rexxfr3dALT  35989  bj-isseti  37363  bj-ceqsalt  37371  bj-ceqsalg  37374  bj-spcimdv  37380  bj-csbsnlem  37388  bj-vtoclg1f  37403  bj-snsetex  37448  bj-snglc  37454  bj-clel3gALT  37533  cgsex2gd  37629  copsex2d  37631  prjspeclsp  43194  elex2VD  45413  elex22VD  45414  tpid3gVD  45417  elsprel  48081