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  3694  elunii  3844  axpweq  4204  euotd  4287  brcogw  4835  opeldmg  4871  breldmg  4872  dmsnopg  5141  dff3im  5707  elunirn  5813  unielxp  6232  op1steq  6237  tfr0dm  6380  tfrlemibxssdm  6385  tfrlemiex  6389  tfr1onlembxssdm  6401  tfr1onlemex  6405  tfrcllembxssdm  6414  tfrcllemex  6418  frecabcl  6457  ertr  6607  f1oen3g  6813  f1dom2g  6815  f1domg  6817  dom3d  6833  en1  6858  phpelm  6927  isinfinf  6958  ordiso  7102  djudom  7159  difinfsn  7166  ctm  7175  enumct  7181  djudoml  7286  djudomr  7287  cc2lem  7333  recexnq  7457  ltexprlemrl  7677  ltexprlemru  7679  recexprlemm  7691  recexprlemloc  7698  recexprlem1ssl  7700  recexprlem1ssu  7701  axpre-suploclemres  7968  frecuzrdgtcl  10504  frecuzrdgfunlem  10511  fihasheqf1oi  10879  zfz1isolem1  10932  climeu  11461  fsum3  11552  uzwodc  12204  gsumfzval  13034  eltg3  14293  uptx  14510  xblm  14653  2lgslem1  15332  bj-2inf  15584  subctctexmid  15645