Theorem spcegv 2861

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

Syntax hints:   -> wi 4   <-> wb 105   = wceq 1373   E.wex 1515   e. wcel 2176

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-v 2774

This theorem is referenced by:  spcedv  2862  spcev  2868  elabd  2918  eqeu  2943  absneu  3705  elunii  3855  axpweq  4216  euotd  4300  brcogw  4848  opeldmg  4884  breldmg  4885  dmsnopg  5155  dff3im  5727  elunirn  5837  unielxp  6262  op1steq  6267  tfr0dm  6410  tfrlemibxssdm  6415  tfrlemiex  6419  tfr1onlembxssdm  6431  tfr1onlemex  6435  tfrcllembxssdm  6444  tfrcllemex  6448  frecabcl  6487  ertr  6637  f1oen4g  6845  f1dom4g  6846  f1oen3g  6847  f1dom2g  6849  f1domg  6851  dom3d  6867  en1  6893  en2  6914  phpelm  6965  isinfinf  6996  ordiso  7140  djudom  7197  difinfsn  7204  ctm  7213  enumct  7219  djudoml  7333  djudomr  7334  cc2lem  7380  recexnq  7505  ltexprlemrl  7725  ltexprlemru  7727  recexprlemm  7739  recexprlemloc  7746  recexprlem1ssl  7748  recexprlem1ssu  7749  axpre-suploclemres  8016  frecuzrdgtcl  10559  frecuzrdgfunlem  10566  fihasheqf1oi  10934  zfz1isolem1  10987  climeu  11640  fsum3  11731  uzwodc  12391  gsumfzval  13256  mplsubgfilemm  14493  eltg3  14562  uptx  14779  xblm  14922  2lgslem1  15601  bj-2inf  15911  subctctexmid  15974