Theorem elisset 2821

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

Syntax hints:   → wi 4   = wceq 1547  ∃wex 1786   ∈ wcel 2119

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-clel 2814

This theorem is referenced by:  ceqsalt  3464  ceqsalgALT  3467  cgsexg  3475  cgsex2g  3476  cgsex4g  3477  vtocleg  3499  vtocld  3506  vtoclg1f  3514  spcimdv  3531  spcegv  3535  spc2egv  3537  spc2ed  3539  eqvincg  3586  clel2g  3597  clel4g  3601  elabd2  3608  elabgt  3610  elabgtOLD  3611  ralsng  4607  dfiun2g  4959  nvel  5241  iinexg  5276  ralxfr2d  5339  copsex2t  5433  dmopab2rex  5859  fliftf  7259  eloprabga  7465  ovmpt4g  7503  eroveu  8749  mreiincl  17549  metustfbas  24540  brabgaf  32698  bnj852  35103  bnj938  35119  bnj1125  35174  bnj1148  35178  bnj1154  35181  fineqvpow  35296  dmopab3rexdif  35633  rexxfr3dALT  35867  bj-isseti  37231  bj-ceqsalt  37239  bj-ceqsalg  37242  bj-spcimdv  37248  bj-csbsnlem  37256  bj-vtoclg1f  37271  bj-snsetex  37316  bj-snglc  37322  bj-clel3gALT  37401  cgsex2gd  37497  copsex2d  37499  prjspeclsp  43062  elex2VD  45281  elex22VD  45282  tpid3gVD  45285  elsprel  47950