Theorem elisset 2740

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

Syntax hints:   → wi 4   = wceq 1343  ∃wex 1480   ∈ wcel 2136  Vcvv 2726

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-v 2728

This theorem is referenced by:  elex22  2741  elex2  2742  ceqsalt  2752  ceqsalg  2754  cgsexg  2761  cgsex2g  2762  cgsex4g  2763  vtoclgft  2776  vtocleg  2797  vtoclegft  2798  spc2egv  2816  spc2gv  2817  spc3egv  2818  spc3gv  2819  eqvincg  2850  tpid3g  3691  iinexgm  4133  copsex2t  4223  copsex2g  4224  ralxfr2d  4442  rexxfr2d  4443  fliftf  5767  eloprabga  5929  ovmpt4g  5964  spc2ed  6201  eroveu  6592  supelti  6967  genpassl  7465  genpassu  7466  eqord1  8381  nn1suc  8876  bj-inex  13789