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  6583  tfrlem9  6594  oawordriexmid  6747  nneneq  7162  diffitest  7195  xpfi  7243  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  10011  infsupneg  10012  ublbneg  10029  fzrevral  10529  zsupcllemex  10680  seq3caopr3  10949  seq3id3  10982  ccatalpha  11403  wrdind  11516  wrd2ind  11517  reuccatpfxs1lem  11540  recan  11898  cau3lem  11903  caubnd2  11906  climshftlemg  12093  subcn2  12102  climcau  12138  serf0  12143  sumdc  12149  isumrpcl  12286  clim2prod  12331  prodmodclem2  12369  ndvdssub  12722  dfgcd3  12812  dfgcd2  12816  coprmgcdb  12891  coprmdvds1  12894  nprm  12926  dvdsprm  12941  coprm  12948  sqrt2irr  12966  pcmpt  13151  pcmptdvds  13153  pcfac  13158  prmpwdvds  13163  lidrididd  13761  dfgrp2  13891  grpidinv2  13922  dfgrp3mlem  13962  issubg4m  14055  srgrz  14395  srglz  14396  srgisid  14397  rrgeq0i  14681  islmodd  14738  rmodislmod  14797  rnglidlmcl  14926  cnpnei  15445  lmss  15472  txlm  15505  psmet0  15553  metss  15720  metcnp3  15737  mulc1cncf  15815  cncfco  15817  chtqub  16296  2sqlem6  16444  2sqlem10  16449  usgruspgrben  16632  wlk1walkdom  16805  wlkres  16825  clwwlkccatlem  16846  clwwlkext2edg  16868  lealltlt1  16956  lealltlt2  16957  bj-indsuc  17159  bj-inf2vnlem2  17202  pw1dceq  17240  wexmiddc  17247  rirrdisj  17291  trirec0  17300  iswomni0  17308  neap0mkv  17326