Theorem elisset 2870

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

Assertion

Ref	Expression
elisset	|- (A e. V -> E.x x = A)

Distinct variable group:   x,A

Allowed substitution hint:   V(x)

Proof of Theorem elisset

Step	Hyp	Ref	Expression
1		elex 2868	. 2 |- (A e. V -> A e. _V)
2		isset 2864	. 2 |- (A e. _V <-> E.x x = A)
3	1, 2	sylib 188	1 |- (A e. V -> E.x x = A)

Syntax hints:   -> wi 4  E.wex 1541   = wceq 1642   e. wcel 1710  _Vcvv 2860

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1542  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-v 2862

This theorem is referenced by:  elex22  2871  elex2  2872  ceqsalt  2882  ceqsalg  2884  cgsexg  2891  cgsex2g  2892  cgsex4g  2893  vtoclgft  2906  vtocleg  2926  vtoclegft  2927  spc2egv  2942  spc3egv  2944  tpid3g  3832  opkelcokg  4262  copsex2t  4609  copsex2g  4610  ovmpt4g  5711  ncelncs  6121