Theorem spcegv 2913

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 2392	. 2 |- F/_ x A
2		nfv 1581	. 2 |- F/ x ps
3		spcgv.1	. 2 |- ( x = A -> ( ph <-> ps ) )
4	1, 2, 3	spcegf 2908	1 |- ( A e. V -> ( ps -> E. x ph ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105   = wceq 1402   E.wex 1545   e. wcel 2209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823

This theorem is used by:  spcedv  2914  spcev  2920  elabd  2971  eqeu  2996  absneu  3783  elunii  3940  axpweq  4308  euotd  4395  brcogw  4949  opeldmg  4986  breldmg  4987  dmsnopg  5259  dff3im  5853  elunirn  5972  unielxp  6408  op1steq  6413  tfr0dm  6593  tfrlemibxssdm  6598  tfrlemiex  6602  tfr1onlembxssdm  6614  tfr1onlemex  6618  tfrcllembxssdm  6627  tfrcllemex  6631  frecabcl  6670  ertr  6822  f1oen4g  7038  f1dom4g  7039  f1oen3g  7040  f1dom2g  7042  f1domg  7044  dom3d  7060  en1  7086  en2  7112  phpelm  7168  isinfinf  7201  ordiso  7376  djudom  7433  difinfsn  7440  ctm  7449  enumct  7455  djudoml  7575  djudomr  7576  cc2lem  7632  recexnq  7757  ltexprlemrl  7977  ltexprlemru  7979  recexprlemm  7991  recexprlemloc  7998  recexprlem1ssl  8000  recexprlem1ssu  8001  axpre-suploclemres  8268  frecuzrdgtcl  10849  frecuzrdgfunlem  10856  fihasheqf1oi  11226  zfz1isolem1  11292  climeu  12062  fsum3  12154  uzwodc  12814  gzsumfzval  13711  mplsubgfilemm  15089  eltg3  15158  uptx  15375  xblm  15518  2lgslem1  16210  upgrex  16344  vtxdumgrfival  16539  1loopgrvd2fi  16546  bj-2inf  16964  subctctexmid  17030