Theorem elisset 2774

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

Syntax hints:   → wi 4   = wceq 1364  ∃wex 1503   ∈ wcel 2164  Vcvv 2760

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-v 2762

This theorem is referenced by:  elex22  2775  elex2  2776  ceqsalt  2786  ceqsalg  2788  cgsexg  2795  cgsex2g  2796  cgsex4g  2797  vtoclgft  2810  vtocleg  2831  vtoclegft  2832  spc2egv  2850  spc2gv  2851  spc3egv  2852  spc3gv  2853  eqvincg  2884  tpid3g  3733  iinexgm  4183  copsex2t  4274  copsex2g  4275  ralxfr2d  4495  rexxfr2d  4496  fliftf  5842  eloprabga  6005  ovmpt4g  6041  spc2ed  6286  eroveu  6680  supelti  7061  genpassl  7584  genpassu  7585  eqord1  8502  nn1suc  9001  bj-inex  15399