Theorem elisset 2624

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

Syntax hints:   → wi 4   = wceq 1285  ∃wex 1422   ∈ wcel 1434  Vcvv 2612

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-ext 2065

This theorem depends on definitions:  df-bi 115  df-sb 1688  df-clab 2070  df-cleq 2076  df-clel 2079  df-v 2614

This theorem is referenced by:  elex22  2625  elex2  2626  ceqsalt  2636  ceqsalg  2638  cgsexg  2645  cgsex2g  2646  cgsex4g  2647  vtoclgft  2660  vtocleg  2680  vtoclegft  2681  spc2egv  2698  spc2gv  2699  spc3egv  2700  spc3gv  2701  eqvincg  2729  tpid3g  3529  iinexgm  3955  copsex2t  4036  copsex2g  4037  ralxfr2d  4250  rexxfr2d  4251  fliftf  5518  eloprabga  5670  ovmpt4g  5702  spc2ed  5933  eroveu  6313  supelti  6604  genpassl  6986  genpassu  6987  nn1suc  8335  bj-inex  11141