Theorem spcegv 2687

Description: Existential specialization, using implicit substitution. (Contributed by NM, 14-Aug-1994.)

Hypothesis

Ref	Expression
spcgv.1	|- ( x = A -> ( ph <-> ps ) )

Assertion

Ref	Expression
spcegv	|- ( A e. V -> ( ps -> E. x ph ) )

Distinct variable groups:   ps, x   x, A

Allowed substitution hints:   ph( x)   V( x)

Proof of Theorem spcegv

Step	Hyp	Ref	Expression
1		nfcv 2220	. 2 |- F/_ x A
2		nfv 1462	. 2 |- F/ x ps
3		spcgv.1	. 2 |- ( x = A -> ( ph <-> ps ) )
4	1, 2, 3	spcegf 2682	1 |- ( A e. V -> ( ps -> E. x ph ) )

Syntax hints:   -> wi 4   <-> wb 103   = wceq 1285   E.wex 1422   e. wcel 1434

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2064

This theorem depends on definitions:  df-bi 115  df-tru 1288  df-nf 1391  df-sb 1687  df-clab 2069  df-cleq 2075  df-clel 2078  df-nfc 2209  df-v 2604

This theorem is referenced by:  spcev  2693  eqeu  2763  absneu  3472  elunii  3614  axpweq  3953  euotd  4017  brcogw  4532  opeldmg  4568  breldmg  4569  dmsnopg  4822  dff3im  5344  elunirn  5437  unielxp  5831  op1steq  5836  tfr0dm  5971  tfrlemibxssdm  5976  tfrlemiex  5980  tfr1onlembxssdm  5992  tfr1onlemex  5996  tfrcllembxssdm  6005  tfrcllemex  6009  frecabcl  6048  ertr  6187  f1oen3g  6301  f1dom2g  6303  f1domg  6305  dom3d  6321  en1  6346  phpelm  6401  ordiso  6506  recexnq  6642  ltexprlemrl  6862  ltexprlemru  6864  recexprlemm  6876  recexprlemloc  6883  recexprlem1ssl  6885  recexprlem1ssu  6886  frecuzrdgtcl  9494  frecuzrdgfunlem  9501  sizeeqf1oi  9812  climeu  10273  bj-2inf  10891