Theorem spcegv 2852

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

Syntax hints:   -> wi 4   <-> wb 105   = wceq 1364   E.wex 1506   e. wcel 2167

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-io 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-v 2765

This theorem is referenced by:  spcedv  2853  spcev  2859  elabd  2909  eqeu  2934  absneu  3695  elunii  3845  axpweq  4205  euotd  4288  brcogw  4836  opeldmg  4872  breldmg  4873  dmsnopg  5142  dff3im  5710  elunirn  5816  unielxp  6241  op1steq  6246  tfr0dm  6389  tfrlemibxssdm  6394  tfrlemiex  6398  tfr1onlembxssdm  6410  tfr1onlemex  6414  tfrcllembxssdm  6423  tfrcllemex  6427  frecabcl  6466  ertr  6616  f1oen3g  6822  f1dom2g  6824  f1domg  6826  dom3d  6842  en1  6867  phpelm  6936  isinfinf  6967  ordiso  7111  djudom  7168  difinfsn  7175  ctm  7184  enumct  7190  djudoml  7302  djudomr  7303  cc2lem  7349  recexnq  7474  ltexprlemrl  7694  ltexprlemru  7696  recexprlemm  7708  recexprlemloc  7715  recexprlem1ssl  7717  recexprlem1ssu  7718  axpre-suploclemres  7985  frecuzrdgtcl  10521  frecuzrdgfunlem  10528  fihasheqf1oi  10896  zfz1isolem1  10949  climeu  11478  fsum3  11569  uzwodc  12229  gsumfzval  13093  eltg3  14377  uptx  14594  xblm  14737  2lgslem1  15416  bj-2inf  15668  subctctexmid  15731