Theorem rspcv 2830

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

Syntax hints:   -> wi 4   <-> wb 104   = wceq 1348   e. wcel 2141   A.wral 2448

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ral 2453  df-v 2732

This theorem is referenced by:  rspccv  2831  rspcva  2832  rspccva  2833  rspcdva  2839  rspc3v  2850  rr19.3v  2869  rr19.28v  2870  rspsbc  3037  rspc2vd  3117  intmin  3849  ralxfrALT  4450  ontr2exmid  4507  reg2exmidlema  4516  0elsucexmid  4547  funcnvuni  5265  acexmidlemcase  5846  tfrlem1  6285  tfrlem9  6296  oawordriexmid  6447  nneneq  6832  diffitest  6862  xpfi  6904  ordiso2  7009  exmidontriimlem3  7189  prnmaxl  7439  prnminu  7440  cauappcvgprlemm  7596  cauappcvgprlemladdru  7607  cauappcvgprlemladdrl  7608  caucvgsrlemcl  7740  caucvgsrlemfv  7742  caucvgsr  7753  axcaucvglemres  7850  lbreu  8850  nnsub  8906  supinfneg  9543  infsupneg  9544  ublbneg  9561  fzrevral  10050  seq3caopr3  10426  seq3id3  10452  recan  11062  cau3lem  11067  caubnd2  11070  climshftlemg  11254  subcn2  11263  climcau  11299  serf0  11304  sumdc  11310  isumrpcl  11446  clim2prod  11491  prodmodclem2  11529  ndvdssub  11878  zsupcllemex  11890  dfgcd3  11954  dfgcd2  11958  coprmgcdb  12031  coprmdvds1  12034  nprm  12066  dvdsprm  12080  coprm  12087  sqrt2irr  12105  pcmpt  12284  pcmptdvds  12286  pcfac  12291  prmpwdvds  12296  lidrididd  12625  dfgrp2  12721  cnpnei  12974  lmss  13001  txlm  13034  psmet0  13082  metss  13249  metcnp3  13266  mulc1cncf  13331  cncfco  13333  2sqlem6  13711  2sqlem10  13716  bj-indsuc  13925  bj-inf2vnlem2  13968  trirec0  14038  iswomni0  14045