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  2811  vtocleg  2832  vtoclegft  2833  spc2egv  2851  spc2gv  2852  spc3egv  2853  spc3gv  2854  eqvincg  2885  tpid3g  3734  iinexgm  4184  copsex2t  4275  copsex2g  4276  ralxfr2d  4496  rexxfr2d  4497  fliftf  5843  eloprabga  6006  ovmpt4g  6042  spc2ed  6288  eroveu  6682  supelti  7063  genpassl  7586  genpassu  7587  eqord1  8504  nn1suc  9003  bj-inex  15469