Theorem elisset 2777

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

Syntax hints:   → wi 4   = wceq 1364  ∃wex 1506   ∈ wcel 2167  Vcvv 2763

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-v 2765

This theorem is referenced by:  elex22  2778  elex2  2779  ceqsalt  2789  ceqsalg  2791  cgsexg  2798  cgsex2g  2799  cgsex4g  2800  vtoclgft  2814  vtocleg  2835  vtoclegft  2836  spc2egv  2854  spc2gv  2855  spc3egv  2856  spc3gv  2857  eqvincg  2888  tpid3g  3737  iinexgm  4187  copsex2t  4278  copsex2g  4279  ralxfr2d  4499  rexxfr2d  4500  fliftf  5846  eloprabga  6009  ovmpt4g  6045  spc2ed  6291  eroveu  6685  supelti  7068  genpassl  7591  genpassu  7592  eqord1  8510  nn1suc  9009  bj-inex  15553