Theorem elisset 3433

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

Syntax hints:   → wi 4   = wceq 1658  ∃wex 1880   ∈ wcel 2166  Vcvv 3415

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-12 2222  ax-ext 2804

This theorem depends on definitions:  df-bi 199  df-an 387  df-tru 1662  df-ex 1881  df-sb 2070  df-clab 2813  df-cleq 2819  df-clel 2822  df-v 3417

This theorem is referenced by:  elex2  3434  elex22  3435  ceqsalt  3446  ceqsalgALT  3449  cgsexg  3456  cgsex2g  3457  cgsex4g  3458  vtoclgft  3472  vtocleg  3497  vtoclegft  3498  spc2egv  3513  spc3egv  3515  eqvincg  3548  iinexg  5047  ralxfr2d  5111  copsex2t  5178  copsex2g  5179  fliftf  6821  eloprabga  7008  ovmpt4g  7044  eroveu  8109  mreiincl  16610  metustfbas  22733  spc2ed  29868  brabgaf  29968  bnj852  31538  bnj938  31554  bnj1125  31607  bnj1148  31611  bnj1154  31614  bj-csbsnlem  33420  bj-snsetex  33474  bj-snglc  33480  elex2VD  39893  elex22VD  39894  tpid3gVD  39897  elsprel  42573