Theorem rspcv 2719

Description: Restricted specialization, using implicit substitution. (Contributed by NM, 26-May-1998.)

Hypothesis

Ref	Expression
rspcv.1	|- ( x = A -> ( ph <-> ps ) )

Assertion

Ref	Expression
rspcv	|- ( A e. B -> ( A. x e. B ph -> ps ) )

Distinct variable groups:   x, A   x, B   ps, x

Allowed substitution hint:   ph( x)

Proof of Theorem rspcv

Step	Hyp	Ref	Expression
1		nfv 1467	. 2 |- F/ x ps
2		rspcv.1	. 2 |- ( x = A -> ( ph <-> ps ) )
3	1, 2	rspc 2717	1 |- ( A e. B -> ( A. x e. B ph -> ps ) )

Syntax hints:   -> wi 4   <-> wb 104   = wceq 1290   e. wcel 1439   A.wral 2360

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 666  ax-5 1382  ax-7 1383  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-8 1441  ax-10 1442  ax-11 1443  ax-i12 1444  ax-bndl 1445  ax-4 1446  ax-17 1465  ax-i9 1469  ax-ial 1473  ax-i5r 1474  ax-ext 2071

This theorem depends on definitions:  df-bi 116  df-tru 1293  df-nf 1396  df-sb 1694  df-clab 2076  df-cleq 2082  df-clel 2085  df-nfc 2218  df-ral 2365  df-v 2622

This theorem is referenced by:  rspccv  2720  rspcva  2721  rspccva  2722  rspcdva  2728  rspc3v  2738  rr19.3v  2756  rr19.28v  2757  rspsbc  2922  intmin  3714  ralxfrALT  4302  ontr2exmid  4354  reg2exmidlema  4363  0elsucexmid  4394  funcnvuni  5096  acexmidlemcase  5661  tfrlem1  6087  tfrlem9  6098  oawordriexmid  6245  nneneq  6627  diffitest  6657  xpfi  6694  ordiso2  6782  prnmaxl  7108  prnminu  7109  cauappcvgprlemm  7265  cauappcvgprlemladdru  7276  cauappcvgprlemladdrl  7277  caucvgsrlemcl  7395  caucvgsrlemfv  7397  caucvgsr  7408  axcaucvglemres  7495  lbreu  8467  nnsub  8522  supinfneg  9144  infsupneg  9145  ublbneg  9159  fzrevral  9580  iseqval  9932  iseqfeq  9957  iseqcaopr3  9971  iseqid3s  9999  recan  10603  cau3lem  10608  caubnd2  10611  climshftlemg  10751  subcn2  10761  climcau  10797  serf0  10802  sumdc  10808  isumrpcl  10949  ndvdssub  11269  zsupcllemex  11281  dfgcd3  11338  dfgcd2  11342  coprmgcdb  11409  coprmdvds1  11412  nprm  11444  dvdsprm  11457  coprm  11462  sqrt2irr  11480  mulc1cncf  11918  cncfco  11920  bj-indsuc  12096  bj-inf2vnlem2  12139