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  4613  ontr2exmid  4672  reg2exmidlema  4681  0elsucexmid  4712  funcnvuni  5450  acexmidlemcase  6080  suppfnss  6497  tfrlem1  6579  tfrlem9  6590  oawordriexmid  6743  nneneq  7158  diffitest  7191  xpfi  7239  ordiso2  7375  exmidontriimlem3  7579  prnmaxl  7855  prnminu  7856  cauappcvgprlemm  8012  cauappcvgprlemladdru  8023  cauappcvgprlemladdrl  8024  caucvgsrlemcl  8156  caucvgsrlemfv  8158  caucvgsr  8169  axcaucvglemres  8266  lbreu  9275  nnsub  9343  supinfneg  9995  infsupneg  9996  ublbneg  10013  fzrevral  10512  zsupcllemex  10663  seq3caopr3  10928  seq3id3  10961  ccatalpha  11381  wrdind  11494  wrd2ind  11495  reuccatpfxs1lem  11518  recan  11875  cau3lem  11880  caubnd2  11883  climshftlemg  12068  subcn2  12077  climcau  12113  serf0  12118  sumdc  12124  isumrpcl  12261  clim2prod  12306  prodmodclem2  12344  ndvdssub  12697  dfgcd3  12787  dfgcd2  12791  coprmgcdb  12866  coprmdvds1  12869  nprm  12901  dvdsprm  12915  coprm  12922  sqrt2irr  12940  pcmpt  13122  pcmptdvds  13124  pcfac  13129  prmpwdvds  13134  lidrididd  13702  dfgrp2  13832  grpidinv2  13863  dfgrp3mlem  13903  issubg4m  13996  srgrz  14288  srglz  14289  srgisid  14290  rrgeq0i  14572  islmodd  14629  rmodislmod  14688  rnglidlmcl  14817  cnpnei  15320  lmss  15347  txlm  15380  psmet0  15428  metss  15595  metcnp3  15612  mulc1cncf  15690  cncfco  15692  2sqlem6  16239  2sqlem10  16244  usgruspgrben  16427  wlk1walkdom  16600  wlkres  16620  clwwlkccatlem  16641  clwwlkext2edg  16663  lealltlt1  16751  lealltlt2  16752  bj-indsuc  16954  bj-inf2vnlem2  16997  pw1dceq  17035  wexmiddc  17042  trirec0  17093  iswomni0  17101  neap0mkv  17119