Theorem elisset 2811

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

Syntax hints:   → wi 4   = wceq 1540  ∃wex 1779   ∈ wcel 2109

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-clel 2804

This theorem is referenced by:  ceqsalt  3484  ceqsalgALT  3487  cgsexg  3495  cgsex2g  3496  cgsex4g  3497  cgsex4gOLD  3498  vtocleg  3522  vtocld  3530  vtoclg1f  3539  vtoclgOLD  3540  vtoclegftOLD  3558  spcimdv  3562  spcegv  3566  spc2egv  3568  spc2ed  3570  eqvincg  3617  clel2g  3628  clel4g  3632  elabd2  3639  elabgt  3641  elabgtOLD  3642  elabgtOLDOLD  3643  ralsng  4642  dfiun2g  4997  iinexg  5306  ralxfr2d  5368  copsex2t  5455  dmopab2rex  5884  fliftf  7293  eloprabga  7501  ovmpt4g  7539  eroveu  8788  mreiincl  17564  metustfbas  24452  brabgaf  32543  bnj852  34918  bnj938  34934  bnj1125  34989  bnj1148  34993  bnj1154  34996  fineqvpow  35093  dmopab3rexdif  35399  rexxfr3dALT  35633  bj-isseti  36873  bj-ceqsalt  36881  bj-ceqsalg  36884  bj-spcimdv  36890  bj-csbsnlem  36898  bj-vtoclg1f  36913  bj-snsetex  36958  bj-snglc  36964  bj-clel3gALT  37043  copsex2d  37134  prjspeclsp  42607  elex2VD  44834  elex22VD  44835  tpid3gVD  44838  elsprel  47480