Theorem elisset 3215

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

Syntax hints:   -> wi 4   = wceq 1483   E.wex 1704   e. wcel 1990   _Vcvv 3200

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-12 2047  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-tru 1486  df-ex 1705  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-v 3202

This theorem is referenced by:  elex2  3216  elex22  3217  ceqsalt  3228  ceqsalgALT  3231  cgsexg  3238  cgsex2g  3239  cgsex4g  3240  vtoclgft  3254  vtoclgftOLD  3255  vtocleg  3279  vtoclegft  3280  spc2egv  3295  spc3egv  3297  eqvincg  3329  tpid3gOLD  4306  iinexg  4824  ralxfr2d  4882  copsex2t  4957  copsex2g  4958  fliftf  6565  eloprabga  6747  ovmpt4g  6783  eroveu  7842  mreiincl  16256  metustfbas  22362  spc2ed  29312  brabgaf  29420  bnj852  30991  bnj938  31007  bnj1125  31060  bnj1148  31064  bnj1154  31067  bj-csbsnlem  32898  bj-snsetex  32951  bj-snglc  32957  elex2VD  39073  elex22VD  39074  tpid3gVD  39077  elsprel  41725