Theorem elisset 2818

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

Syntax hints:   → wi 4   = wceq 1542  ∃wex 1781   ∈ wcel 2114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-clel 2811

This theorem is referenced by:  ceqsalt  3463  ceqsalgALT  3466  cgsexg  3474  cgsex2g  3475  cgsex4g  3476  vtocleg  3498  vtocld  3506  vtoclg1f  3514  spcimdv  3535  spcegv  3539  spc2egv  3541  spc2ed  3543  eqvincg  3590  clel2g  3601  clel4g  3605  elabd2  3612  elabgt  3614  elabgtOLD  3615  elabgtOLDOLD  3616  ralsng  4619  dfiun2g  4972  nvel  5254  iinexg  5289  ralxfr2d  5352  copsex2t  5446  dmopab2rex  5872  fliftf  7270  eloprabga  7476  ovmpt4g  7514  eroveu  8759  mreiincl  17558  metustfbas  24522  brabgaf  32679  bnj852  35063  bnj938  35079  bnj1125  35134  bnj1148  35138  bnj1154  35141  fineqvpow  35259  dmopab3rexdif  35587  rexxfr3dALT  35821  bj-isseti  37185  bj-ceqsalt  37193  bj-ceqsalg  37196  bj-spcimdv  37202  bj-csbsnlem  37210  bj-vtoclg1f  37225  bj-snsetex  37270  bj-snglc  37276  bj-clel3gALT  37355  cgsex2gd  37451  copsex2d  37453  prjspeclsp  43045  elex2VD  45264  elex22VD  45265  tpid3gVD  45268  elsprel  47935