Theorem elisset 2777

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 2774	. 2 |- ( A e. V -> A e. _V )
2		isset 2769	. 2 |- ( A e. _V <-> E. x x = A )
3	1, 2	sylib 122	1 |- ( A e. V -> E. x x = A )

Syntax hints:   -> wi 4   = wceq 1364   E.wex 1506   e. wcel 2167   _Vcvv 2763

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-v 2765

This theorem is referenced by:  elex22  2778  elex2  2779  ceqsalt  2789  ceqsalg  2791  cgsexg  2798  cgsex2g  2799  cgsex4g  2800  vtoclgft  2814  vtocleg  2835  vtoclegft  2836  spc2egv  2854  spc2gv  2855  spc3egv  2856  spc3gv  2857  eqvincg  2888  tpid3g  3738  iinexgm  4188  copsex2t  4279  copsex2g  4280  ralxfr2d  4500  rexxfr2d  4501  fliftf  5849  eloprabga  6013  ovmpt4g  6049  spc2ed  6300  eroveu  6694  supelti  7077  genpassl  7608  genpassu  7609  eqord1  8527  nn1suc  9026  bj-inex  15637