Theorem rspcv 2925

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

This proof depends on syntax axioms:   -> wi 4   <-> wb 105   = wceq 1402   e. wcel 2209   A.wral 2528

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ral 2533  df-v 2823

This theorem is used by:  rspccv  2926  rspcva  2927  rspccva  2928  rspcdva  2934  rspc3v  2946  rr19.3v  2965  rr19.28v  2966  rspsbc  3135  rspc2vd  3216  intmin  3990  ralxfrALT  4615  ontr2exmid  4674  reg2exmidlema  4683  0elsucexmid  4714  funcnvuni  5453  acexmidlemcase  6083  suppfnss  6501  tfrlem1  6584  tfrlem9  6595  oawordriexmid  6748  nneneq  7164  diffitest  7197  xpfi  7245  ordiso2  7381  exmidontriimlem3  7585  prnmaxl  7861  prnminu  7862  cauappcvgprlemm  8018  cauappcvgprlemladdru  8029  cauappcvgprlemladdrl  8030  caucvgsrlemcl  8162  caucvgsrlemfv  8164  caucvgsr  8175  axcaucvglemres  8272  lbreu  9283  nnsub  9352  supinfneg  10010  infsupneg  10011  ublbneg  10028  fzrevral  10528  zsupcllemex  10679  seq3caopr3  10948  seq3id3  10981  ccatalpha  11402  wrdind  11515  wrd2ind  11516  reuccatpfxs1lem  11539  recan  11897  cau3lem  11902  caubnd2  11905  climshftlemg  12092  subcn2  12101  climcau  12137  serf0  12142  sumdc  12148  isumrpcl  12285  clim2prod  12330  prodmodclem2  12368  ndvdssub  12721  dfgcd3  12811  dfgcd2  12815  coprmgcdb  12890  coprmdvds1  12893  nprm  12925  dvdsprm  12940  coprm  12947  sqrt2irr  12965  pcmpt  13150  pcmptdvds  13152  pcfac  13157  prmpwdvds  13162  lidrididd  13760  dfgrp2  13890  grpidinv2  13921  dfgrp3mlem  13961  issubg4m  14054  srgrz  14394  srglz  14395  srgisid  14396  rrgeq0i  14680  islmodd  14737  rmodislmod  14796  rnglidlmcl  14925  mvrf1fi  15219  cnpnei  15462  lmss  15489  txlm  15522  psmet0  15570  metss  15737  metcnp3  15754  mulc1cncf  15832  cncfco  15834  chtqub  16313  2sqlem6  16461  2sqlem10  16466  usgruspgrben  16649  wlk1walkdom  16822  wlkres  16842  clwwlkccatlem  16863  clwwlkext2edg  16885  lealltlt1  16973  lealltlt2  16974  bj-indsuc  17176  bj-inf2vnlem2  17219  pw1dceq  17257  wexmiddc  17264  rirrdisj  17308  trirec0  17317  iswomni0  17325  neap0mkv  17343