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  4310  euotd  4397  brcogw  4951  opeldmg  4988  breldmg  4989  dmsnopg  5262  dff3im  5856  elunirn  5975  unielxp  6412  op1steq  6417  tfr0dm  6597  tfrlemibxssdm  6602  tfrlemiex  6606  tfr1onlembxssdm  6618  tfr1onlemex  6622  tfrcllembxssdm  6631  tfrcllemex  6635  frecabcl  6674  ertr  6826  f1oen4g  7042  f1dom4g  7043  f1oen3g  7044  f1dom2g  7046  f1domg  7048  dom3d  7064  en1  7090  en2  7116  phpelm  7172  isinfinf  7205  ordiso  7382  djudom  7439  difinfsn  7446  ctm  7455  enumct  7461  djudoml  7581  djudomr  7582  cc2lem  7638  recexnq  7763  ltexprlemrl  7983  ltexprlemru  7985  recexprlemm  7997  recexprlemloc  8004  recexprlem1ssl  8006  recexprlem1ssu  8007  axpre-suploclemres  8274  frecuzrdgtcl  10870  frecuzrdgfunlem  10877  fihasheqf1oi  11248  zfz1isolem1  11314  climeu  12087  fsum3  12179  uzwodc  12839  gzsumfzval  13770  mplsubgfilemm  15214  eltg3  15283  uptx  15500  xblm  15643  2lgslem1  16415  upgrex  16549  vtxdumgrfival  16744  1loopgrvd2fi  16751  bj-2inf  17169  subctctexmid  17235