Theorem elisset 2669

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

Syntax hints:   -> wi 4   = wceq 1312   E.wex 1449   e. wcel 1461   _Vcvv 2655

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1404  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-8 1463  ax-4 1468  ax-17 1487  ax-i9 1491  ax-ial 1495  ax-ext 2095

This theorem depends on definitions:  df-bi 116  df-sb 1717  df-clab 2100  df-cleq 2106  df-clel 2109  df-v 2657

This theorem is referenced by:  elex22  2670  elex2  2671  ceqsalt  2681  ceqsalg  2683  cgsexg  2690  cgsex2g  2691  cgsex4g  2692  vtoclgft  2705  vtocleg  2726  vtoclegft  2727  spc2egv  2744  spc2gv  2745  spc3egv  2746  spc3gv  2747  eqvincg  2777  tpid3g  3602  iinexgm  4037  copsex2t  4125  copsex2g  4126  ralxfr2d  4343  rexxfr2d  4344  fliftf  5652  eloprabga  5810  ovmpt4g  5845  spc2ed  6082  eroveu  6472  supelti  6839  genpassl  7274  genpassu  7275  eqord1  8158  nn1suc  8643  bj-inex  12788