Theorem elisset 2671

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

Syntax hints:   → wi 4   = wceq 1314  ∃wex 1451   ∈ wcel 1463  Vcvv 2657

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1406  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-ext 2097

This theorem depends on definitions:  df-bi 116  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111  df-v 2659

This theorem is referenced by:  elex22  2672  elex2  2673  ceqsalt  2683  ceqsalg  2685  cgsexg  2692  cgsex2g  2693  cgsex4g  2694  vtoclgft  2707  vtocleg  2728  vtoclegft  2729  spc2egv  2746  spc2gv  2747  spc3egv  2748  spc3gv  2749  eqvincg  2779  tpid3g  3604  iinexgm  4039  copsex2t  4127  copsex2g  4128  ralxfr2d  4345  rexxfr2d  4346  fliftf  5654  eloprabga  5812  ovmpt4g  5847  spc2ed  6084  eroveu  6474  supelti  6841  genpassl  7280  genpassu  7281  eqord1  8164  nn1suc  8649  bj-inex  12797