Theorem rspcv 2860

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 1539	. 2 |- F/ x ps
2		rspcv.1	. 2 |- ( x = A -> ( ph <-> ps ) )
3	1, 2	rspc 2858	1 |- ( A e. B -> ( A. x e. B ph -> ps ) )

Syntax hints:   -> wi 4   <-> wb 105   = wceq 1364   e. wcel 2164   A.wral 2472

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ral 2477  df-v 2762

This theorem is referenced by:  rspccv  2861  rspcva  2862  rspccva  2863  rspcdva  2869  rspc3v  2880  rr19.3v  2899  rr19.28v  2900  rspsbc  3068  rspc2vd  3149  intmin  3890  ralxfrALT  4498  ontr2exmid  4557  reg2exmidlema  4566  0elsucexmid  4597  funcnvuni  5323  acexmidlemcase  5913  tfrlem1  6361  tfrlem9  6372  oawordriexmid  6523  nneneq  6913  diffitest  6943  xpfi  6986  ordiso2  7094  exmidontriimlem3  7283  prnmaxl  7548  prnminu  7549  cauappcvgprlemm  7705  cauappcvgprlemladdru  7716  cauappcvgprlemladdrl  7717  caucvgsrlemcl  7849  caucvgsrlemfv  7851  caucvgsr  7862  axcaucvglemres  7959  lbreu  8964  nnsub  9021  supinfneg  9660  infsupneg  9661  ublbneg  9678  fzrevral  10171  seq3caopr3  10562  seq3id3  10595  recan  11253  cau3lem  11258  caubnd2  11261  climshftlemg  11445  subcn2  11454  climcau  11490  serf0  11495  sumdc  11501  isumrpcl  11637  clim2prod  11682  prodmodclem2  11720  ndvdssub  12071  zsupcllemex  12083  dfgcd3  12147  dfgcd2  12151  coprmgcdb  12226  coprmdvds1  12229  nprm  12261  dvdsprm  12275  coprm  12282  sqrt2irr  12300  pcmpt  12481  pcmptdvds  12483  pcfac  12488  prmpwdvds  12493  lidrididd  12965  dfgrp2  13099  grpidinv2  13130  dfgrp3mlem  13170  issubg4m  13263  srgrz  13480  srglz  13481  srgisid  13482  rrgeq0i  13760  islmodd  13789  rmodislmod  13847  rnglidlmcl  13976  cnpnei  14387  lmss  14414  txlm  14447  psmet0  14495  metss  14662  metcnp3  14679  mulc1cncf  14744  cncfco  14746  2sqlem6  15207  2sqlem10  15212  bj-indsuc  15420  bj-inf2vnlem2  15463  trirec0  15534  iswomni0  15541  neap0mkv  15559