Theorem elisset 2544

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 2542	. 2 ⊢ (A ∈ 𝑉 → A ∈ V)
2		isset 2538	. 2 ⊢ (A ∈ V ↔ ∃x x = A)
3	1, 2	sylib 127	1 ⊢ (A ∈ 𝑉 → ∃x x = A)

Syntax hints:   → wi 4  ∃wex 1362   = wceq 1374   ∈ wcel 1376  Vcvv 2534

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 1316  ax-gen 1318  ax-ie1 1363  ax-ie2 1364  ax-8 1378  ax-4 1383  ax-17 1402  ax-i9 1406  ax-ial 1411  ax-ext 2005

This theorem depends on definitions:  df-bi 110  df-sb 1629  df-clab 2010  df-cleq 2016  df-clel 2019  df-v 2536

This theorem is referenced by:  elex22  2545  elex2  2546  ceqsalt  2556  ceqsalg  2558  cgsexg  2565  cgsex2g  2566  cgsex4g  2567  vtoclgft  2580  vtocleg  2600  vtoclegft  2601  spc2egv  2618  spc2gv  2619  spc3egv  2620  spc3gv  2621  eqvincg  2644  tpid3g  3435  iinexgm  3861  copsex2t  3935  copsex2g  3936  ralxfr2d  4122  rexxfr2d  4123  fliftf  5341  eloprabga  5493  ovmpt4g  5525  eroveu  6078