Theorem elisset 2820

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

Syntax hints:   → wi 4   = wceq 1536  ∃wex 1775   ∈ wcel 2105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-clel 2813

This theorem is referenced by:  elex2OLD  3502  ceqsalt  3512  ceqsalgALT  3515  cgsexg  3523  cgsex2g  3524  cgsex4g  3525  cgsex4gOLD  3526  vtocleg  3552  vtocld  3560  vtoclg1f  3569  vtoclgOLD  3570  vtoclegftOLD  3588  spcimdv  3592  spcegv  3596  spc2egv  3598  spc2ed  3600  eqvincg  3647  clel2g  3658  clel4g  3662  elabd2  3669  elabgt  3671  elabgtOLD  3672  elabg  3676  ralsng  4679  dfiun2g  5034  iinexg  5353  ralxfr2d  5415  copsex2t  5502  dmopab2rex  5930  fliftf  7334  eloprabga  7540  eloprabgaOLD  7541  ovmpt4g  7579  eroveu  8850  mreiincl  17640  metustfbas  24585  brabgaf  32627  bnj852  34913  bnj938  34929  bnj1125  34984  bnj1148  34988  bnj1154  34991  fineqvpow  35088  dmopab3rexdif  35389  rexxfr3dALT  35623  bj-isseti  36860  bj-ceqsalt  36868  bj-ceqsalg  36871  bj-spcimdv  36877  bj-csbsnlem  36885  bj-vtoclg1f  36900  bj-snsetex  36945  bj-snglc  36951  bj-clel3gALT  37030  copsex2d  37121  prjspeclsp  42598  elex2VD  44835  elex22VD  44836  tpid3gVD  44839  elsprel  47399