Theorem elisset 2753

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 2750	. 2 |- ( A e. V -> A e. _V )
2		isset 2745	. 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 1353   E.wex 1492   e. wcel 2148   _Vcvv 2739

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-v 2741

This theorem is referenced by:  elex22  2754  elex2  2755  ceqsalt  2765  ceqsalg  2767  cgsexg  2774  cgsex2g  2775  cgsex4g  2776  vtoclgft  2789  vtocleg  2810  vtoclegft  2811  spc2egv  2829  spc2gv  2830  spc3egv  2831  spc3gv  2832  eqvincg  2863  tpid3g  3709  iinexgm  4156  copsex2t  4247  copsex2g  4248  ralxfr2d  4466  rexxfr2d  4467  fliftf  5802  eloprabga  5964  ovmpt4g  5999  spc2ed  6236  eroveu  6628  supelti  7003  genpassl  7525  genpassu  7526  eqord1  8442  nn1suc  8940  bj-inex  14744