Theorem elisset 2532

Description: An element of a class exists. (Contributed by NM, 1-May-1995.)

Assertion

Ref	Expression
elisset	⊢ (A ∈ 𝑉 → ∃x x = A)

Distinct variable group:   x,A

Allowed substitution hint:   𝑉(x)

Proof of Theorem elisset

Step	Hyp	Ref	Expression
1		elex 2530	. 2 ⊢ (A ∈ 𝑉 → A ∈ V)
2		isset 2526	. 2 ⊢ (A ∈ V ↔ ∃x x = A)
3	1, 2	sylib 127	1 ⊢ (A ∈ 𝑉 → ∃x x = A)

Syntax hints:   → wi 4   = wceq 1219  ∃wex 1350   ∈ wcel 1362  Vcvv 2522

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 1305  ax-gen 1307  ax-ie1 1351  ax-ie2 1352  ax-8 1364  ax-4 1369  ax-17 1388  ax-i9 1392  ax-ial 1396  ax-ext 1991

This theorem depends on definitions:  df-bi 110  df-sb 1615  df-clab 1996  df-cleq 2002  df-clel 2005  df-v 2524

This theorem is referenced by:  elex22  2533  elex2  2534  ceqsalt  2544  ceqsalg  2546  cgsexg  2553  cgsex2g  2554  cgsex4g  2555  vtoclgft  2568  vtocleg  2588  vtoclegft  2589  spc2egv  2606  spc2gv  2607  spc3egv  2608  spc3gv  2609  eqvincg  2632  tpid3g  3442  iinexgm  3867  copsex2t  3941  copsex2g  3942  ralxfr2d  4130  rexxfr2d  4131  fliftf  5348  eloprabga  5498  ovmpt4g  5530  eroveu  6092  genpassl  6361  genpassu  6362  bj-inex  7364