Theorem rspcv 2906

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

Syntax hints:   -> wi 4   <-> wb 105   = wceq 1397   e. wcel 2202   A.wral 2510

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ral 2515  df-v 2804

This theorem is referenced by:  rspccv  2907  rspcva  2908  rspccva  2909  rspcdva  2915  rspc3v  2926  rr19.3v  2945  rr19.28v  2946  rspsbc  3115  rspc2vd  3196  intmin  3948  ralxfrALT  4564  ontr2exmid  4623  reg2exmidlema  4632  0elsucexmid  4663  funcnvuni  5399  acexmidlemcase  6013  tfrlem1  6474  tfrlem9  6485  oawordriexmid  6638  nneneq  7043  diffitest  7076  xpfi  7124  ordiso2  7234  exmidontriimlem3  7438  prnmaxl  7708  prnminu  7709  cauappcvgprlemm  7865  cauappcvgprlemladdru  7876  cauappcvgprlemladdrl  7877  caucvgsrlemcl  8009  caucvgsrlemfv  8011  caucvgsr  8022  axcaucvglemres  8119  lbreu  9125  nnsub  9182  supinfneg  9829  infsupneg  9830  ublbneg  9847  fzrevral  10340  zsupcllemex  10490  seq3caopr3  10753  seq3id3  10786  ccatalpha  11190  wrdind  11303  wrd2ind  11304  reuccatpfxs1lem  11327  recan  11670  cau3lem  11675  caubnd2  11678  climshftlemg  11863  subcn2  11872  climcau  11908  serf0  11913  sumdc  11919  isumrpcl  12056  clim2prod  12101  prodmodclem2  12139  ndvdssub  12492  dfgcd3  12582  dfgcd2  12586  coprmgcdb  12661  coprmdvds1  12664  nprm  12696  dvdsprm  12710  coprm  12717  sqrt2irr  12735  pcmpt  12917  pcmptdvds  12919  pcfac  12924  prmpwdvds  12929  lidrididd  13466  dfgrp2  13611  grpidinv2  13642  dfgrp3mlem  13682  issubg4m  13781  srgrz  13999  srglz  14000  srgisid  14001  rrgeq0i  14280  islmodd  14309  rmodislmod  14367  rnglidlmcl  14496  cnpnei  14945  lmss  14972  txlm  15005  psmet0  15053  metss  15220  metcnp3  15237  mulc1cncf  15315  cncfco  15317  2sqlem6  15851  2sqlem10  15856  usgruspgrben  16039  wlk1walkdom  16212  wlkres  16232  clwwlkccatlem  16253  clwwlkext2edg  16275  bj-indsuc  16526  bj-inf2vnlem2  16569  pw1dceq  16608  trirec0  16651  iswomni0  16658  neap0mkv  16676