Theorem elisset 2785

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 2782	. 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V)
2		isset 2777	. 2 ⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
3	1, 2	sylib 122	1 ⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴)

Syntax hints:   → wi 4   = wceq 1372  ∃wex 1514   ∈ wcel 2175  Vcvv 2771

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 1469  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-v 2773

This theorem is referenced by:  elex22  2786  elex2  2787  ceqsalt  2797  ceqsalg  2799  cgsexg  2806  cgsex2g  2807  cgsex4g  2808  vtoclgft  2822  vtocleg  2843  vtoclegft  2844  spc2egv  2862  spc2gv  2863  spc3egv  2864  spc3gv  2865  eqvincg  2896  tpid3g  3747  iinexgm  4197  copsex2t  4288  copsex2g  4289  ralxfr2d  4510  rexxfr2d  4511  fliftf  5867  eloprabga  6031  ovmpt4g  6067  spc2ed  6318  eroveu  6712  supelti  7103  genpassl  7636  genpassu  7637  eqord1  8555  nn1suc  9054  bj-inex  15776