Theorem elisset 2788

Description: An element of a class exists. (Contributed by NM, 1-May-1995.)

Assertion

Ref	Expression
elisset	⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴)

Distinct variable group:   𝑥,𝐴

Allowed substitution hint:   𝑉(𝑥)

Proof of Theorem elisset

Step	Hyp	Ref	Expression
1		elex 2785	. 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V)
2		isset 2780	. 2 ⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
3	1, 2	sylib 122	1 ⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴)

Syntax hints:   → wi 4   = wceq 1373  ∃wex 1516   ∈ wcel 2177  Vcvv 2773

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-v 2775

This theorem is referenced by:  elex22  2789  elex2  2790  ceqsalt  2800  ceqsalg  2802  cgsexg  2809  cgsex2g  2810  cgsex4g  2811  vtoclgft  2825  vtocleg  2848  vtoclegft  2849  spc2egv  2867  spc2gv  2868  spc3egv  2869  spc3gv  2870  eqvincg  2901  tpid3g  3753  iinexgm  4209  copsex2t  4302  copsex2g  4303  ralxfr2d  4524  rexxfr2d  4525  fliftf  5886  eloprabga  6050  ovmpt4g  6086  spc2ed  6337  eroveu  6731  supelti  7125  genpassl  7667  genpassu  7668  eqord1  8586  nn1suc  9085  bj-inex  16012