Theorem rspcv 2873

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

Syntax hints:   -> wi 4   <-> wb 105   = wceq 1373   e. wcel 2176   A.wral 2484

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-ral 2489  df-v 2774

This theorem is referenced by:  rspccv  2874  rspcva  2875  rspccva  2876  rspcdva  2882  rspc3v  2893  rr19.3v  2912  rr19.28v  2913  rspsbc  3081  rspc2vd  3162  intmin  3905  ralxfrALT  4515  ontr2exmid  4574  reg2exmidlema  4583  0elsucexmid  4614  funcnvuni  5344  acexmidlemcase  5941  tfrlem1  6396  tfrlem9  6407  oawordriexmid  6558  nneneq  6956  diffitest  6986  xpfi  7031  ordiso2  7139  exmidontriimlem3  7337  prnmaxl  7603  prnminu  7604  cauappcvgprlemm  7760  cauappcvgprlemladdru  7771  cauappcvgprlemladdrl  7772  caucvgsrlemcl  7904  caucvgsrlemfv  7906  caucvgsr  7917  axcaucvglemres  8014  lbreu  9020  nnsub  9077  supinfneg  9718  infsupneg  9719  ublbneg  9736  fzrevral  10229  zsupcllemex  10375  seq3caopr3  10638  seq3id3  10671  recan  11453  cau3lem  11458  caubnd2  11461  climshftlemg  11646  subcn2  11655  climcau  11691  serf0  11696  sumdc  11702  isumrpcl  11838  clim2prod  11883  prodmodclem2  11921  ndvdssub  12274  dfgcd3  12364  dfgcd2  12368  coprmgcdb  12443  coprmdvds1  12446  nprm  12478  dvdsprm  12492  coprm  12499  sqrt2irr  12517  pcmpt  12699  pcmptdvds  12701  pcfac  12706  prmpwdvds  12711  lidrididd  13247  dfgrp2  13392  grpidinv2  13423  dfgrp3mlem  13463  issubg4m  13562  srgrz  13779  srglz  13780  srgisid  13781  rrgeq0i  14059  islmodd  14088  rmodislmod  14146  rnglidlmcl  14275  cnpnei  14724  lmss  14751  txlm  14784  psmet0  14832  metss  14999  metcnp3  15016  mulc1cncf  15094  cncfco  15096  2sqlem6  15630  2sqlem10  15635  bj-indsuc  15901  bj-inf2vnlem2  15944  trirec0  16020  iswomni0  16027  neap0mkv  16045