Theorem elisset 2568

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

Syntax hints:   → wi 4   = wceq 1243  ∃wex 1381   ∈ wcel 1393  Vcvv 2557

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-ext 2022

This theorem depends on definitions:  df-bi 110  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-v 2559

This theorem is referenced by:  elex22  2569  elex2  2570  ceqsalt  2580  ceqsalg  2582  cgsexg  2589  cgsex2g  2590  cgsex4g  2591  vtoclgft  2604  vtocleg  2624  vtoclegft  2625  spc2egv  2642  spc2gv  2643  spc3egv  2644  spc3gv  2645  eqvincg  2668  tpid3g  3483  iinexgm  3908  copsex2t  3982  copsex2g  3983  ralxfr2d  4196  rexxfr2d  4197  fliftf  5439  eloprabga  5591  ovmpt4g  5623  eroveu  6197  genpassl  6622  genpassu  6623  nn1suc  7933  bj-inex  10027