Theorem rspcv 2917

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

Syntax hints:   -> wi 4   <-> wb 105   = wceq 1398   e. wcel 2203   A.wral 2520

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ral 2525  df-v 2815

This theorem is referenced by:  rspccv  2918  rspcva  2919  rspccva  2920  rspcdva  2926  rspc3v  2937  rr19.3v  2956  rr19.28v  2957  rspsbc  3126  rspc2vd  3207  intmin  3969  ralxfrALT  4588  ontr2exmid  4647  reg2exmidlema  4656  0elsucexmid  4687  funcnvuni  5425  acexmidlemcase  6045  suppfnss  6457  tfrlem1  6539  tfrlem9  6550  oawordriexmid  6703  nneneq  7111  diffitest  7144  xpfi  7192  ordiso2  7326  exmidontriimlem3  7530  prnmaxl  7803  prnminu  7804  cauappcvgprlemm  7960  cauappcvgprlemladdru  7971  cauappcvgprlemladdrl  7972  caucvgsrlemcl  8104  caucvgsrlemfv  8106  caucvgsr  8117  axcaucvglemres  8214  lbreu  9219  nnsub  9276  supinfneg  9927  infsupneg  9928  ublbneg  9945  fzrevral  10439  zsupcllemex  10590  seq3caopr3  10853  seq3id3  10886  ccatalpha  11301  wrdind  11414  wrd2ind  11415  reuccatpfxs1lem  11438  recan  11794  cau3lem  11799  caubnd2  11802  climshftlemg  11987  subcn2  11996  climcau  12032  serf0  12037  sumdc  12043  isumrpcl  12180  clim2prod  12225  prodmodclem2  12263  ndvdssub  12616  dfgcd3  12706  dfgcd2  12710  coprmgcdb  12785  coprmdvds1  12788  nprm  12820  dvdsprm  12834  coprm  12841  sqrt2irr  12859  pcmpt  13041  pcmptdvds  13043  pcfac  13048  prmpwdvds  13053  lidrididd  13595  dfgrp2  13740  grpidinv2  13771  dfgrp3mlem  13811  issubg4m  13910  srgrz  14128  srglz  14129  srgisid  14130  rrgeq0i  14409  islmodd  14441  rmodislmod  14499  rnglidlmcl  14628  cnpnei  15084  lmss  15111  txlm  15144  psmet0  15192  metss  15359  metcnp3  15376  mulc1cncf  15454  cncfco  15456  2sqlem6  15993  2sqlem10  15998  usgruspgrben  16181  wlk1walkdom  16354  wlkres  16374  clwwlkccatlem  16395  clwwlkext2edg  16417  bj-indsuc  16698  bj-inf2vnlem2  16741  pw1dceq  16778  trirec0  16828  iswomni0  16836  neap0mkv  16855