Theorem elisset 2816

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

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

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 2007  ax-8 2110

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-clel 2809

This theorem is referenced by:  elex2OLD  3484  ceqsalt  3494  ceqsalgALT  3497  cgsexg  3505  cgsex2g  3506  cgsex4g  3507  cgsex4gOLD  3508  vtocleg  3532  vtocld  3540  vtoclg1f  3549  vtoclgOLD  3550  vtoclegftOLD  3568  spcimdv  3572  spcegv  3576  spc2egv  3578  spc2ed  3580  eqvincg  3627  clel2g  3638  clel4g  3642  elabd2  3649  elabgt  3651  elabgtOLD  3652  elabg  3655  ralsng  4651  dfiun2g  5006  iinexg  5318  ralxfr2d  5380  copsex2t  5467  dmopab2rex  5897  fliftf  7308  eloprabga  7516  ovmpt4g  7554  eroveu  8826  mreiincl  17608  metustfbas  24496  brabgaf  32588  bnj852  34952  bnj938  34968  bnj1125  35023  bnj1148  35027  bnj1154  35030  fineqvpow  35127  dmopab3rexdif  35427  rexxfr3dALT  35661  bj-isseti  36896  bj-ceqsalt  36904  bj-ceqsalg  36907  bj-spcimdv  36913  bj-csbsnlem  36921  bj-vtoclg1f  36936  bj-snsetex  36981  bj-snglc  36987  bj-clel3gALT  37066  copsex2d  37157  prjspeclsp  42635  elex2VD  44862  elex22VD  44863  tpid3gVD  44866  elsprel  47489