Theorem elisset 2826

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

Syntax hints:   → wi 4   = wceq 1537  ∃wex 1777   ∈ wcel 2108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-clel 2819

This theorem is referenced by:  elex2OLD  3513  ceqsalt  3523  ceqsalgALT  3526  cgsexg  3536  cgsex2g  3537  cgsex4g  3538  cgsex4gOLD  3539  vtocleg  3565  vtocld  3573  vtoclg1f  3582  vtoclgOLD  3583  vtoclegftOLD  3602  spcimdv  3606  spcegv  3610  spc2egv  3612  spc2ed  3614  eqvincg  3661  clel2g  3672  clel4g  3676  elabd2  3683  elabgt  3685  elabgtOLD  3686  elabg  3690  ralsng  4697  dfiun2g  5053  iinexg  5366  ralxfr2d  5428  copsex2t  5512  dmopab2rex  5942  fliftf  7351  eloprabga  7558  eloprabgaOLD  7559  ovmpt4g  7597  eroveu  8870  mreiincl  17654  metustfbas  24591  brabgaf  32630  bnj852  34897  bnj938  34913  bnj1125  34968  bnj1148  34972  bnj1154  34975  fineqvpow  35072  dmopab3rexdif  35373  rexxfr3dALT  35607  bj-isseti  36844  bj-ceqsalt  36852  bj-ceqsalg  36855  bj-spcimdv  36861  bj-csbsnlem  36869  bj-vtoclg1f  36884  bj-snsetex  36929  bj-snglc  36935  bj-clel3gALT  37014  copsex2d  37105  prjspeclsp  42567  elex2VD  44809  elex22VD  44810  tpid3gVD  44813  elsprel  47349