Theorem elisset 2752

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

Syntax hints:   → wi 4   = wceq 1353  ∃wex 1492   ∈ wcel 2148  Vcvv 2738

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-v 2740

This theorem is referenced by:  elex22  2753  elex2  2754  ceqsalt  2764  ceqsalg  2766  cgsexg  2773  cgsex2g  2774  cgsex4g  2775  vtoclgft  2788  vtocleg  2809  vtoclegft  2810  spc2egv  2828  spc2gv  2829  spc3egv  2830  spc3gv  2831  eqvincg  2862  tpid3g  3708  iinexgm  4155  copsex2t  4246  copsex2g  4247  ralxfr2d  4465  rexxfr2d  4466  fliftf  5800  eloprabga  5962  ovmpt4g  5997  spc2ed  6234  eroveu  6626  supelti  7001  genpassl  7523  genpassu  7524  eqord1  8440  nn1suc  8938  bj-inex  14662