Theorem elisset 2869

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 2867	. 2 |- (A e. V -> A e. _V)
2		isset 2863	. 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 2859

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 2861

This theorem is referenced by:  elex22  2870  elex2  2871  ceqsalt  2881  ceqsalg  2883  cgsexg  2890  cgsex2g  2891  cgsex4g  2892  vtoclgft  2905  vtocleg  2925  vtoclegft  2926  spc2egv  2941  spc3egv  2943  tpid3g  3831  opkelcokg  4261  copsex2t  4608  copsex2g  4609  ovmpt4g  5710  ncelncs  6120