Theorem rspcv 2849

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

Syntax hints:   -> wi 4   <-> wb 105   = wceq 1363   e. wcel 2158   A.wral 2465

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 710  ax-5 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-ext 2169

This theorem depends on definitions:  df-bi 117  df-tru 1366  df-nf 1471  df-sb 1773  df-clab 2174  df-cleq 2180  df-clel 2183  df-nfc 2318  df-ral 2470  df-v 2751

This theorem is referenced by:  rspccv  2850  rspcva  2851  rspccva  2852  rspcdva  2858  rspc3v  2869  rr19.3v  2888  rr19.28v  2889  rspsbc  3057  rspc2vd  3137  intmin  3876  ralxfrALT  4479  ontr2exmid  4536  reg2exmidlema  4545  0elsucexmid  4576  funcnvuni  5297  acexmidlemcase  5883  tfrlem1  6322  tfrlem9  6333  oawordriexmid  6484  nneneq  6870  diffitest  6900  xpfi  6942  ordiso2  7047  exmidontriimlem3  7235  prnmaxl  7500  prnminu  7501  cauappcvgprlemm  7657  cauappcvgprlemladdru  7668  cauappcvgprlemladdrl  7669  caucvgsrlemcl  7801  caucvgsrlemfv  7803  caucvgsr  7814  axcaucvglemres  7911  lbreu  8915  nnsub  8971  supinfneg  9608  infsupneg  9609  ublbneg  9626  fzrevral  10118  seq3caopr3  10494  seq3id3  10520  recan  11131  cau3lem  11136  caubnd2  11139  climshftlemg  11323  subcn2  11332  climcau  11368  serf0  11373  sumdc  11379  isumrpcl  11515  clim2prod  11560  prodmodclem2  11598  ndvdssub  11948  zsupcllemex  11960  dfgcd3  12024  dfgcd2  12028  coprmgcdb  12101  coprmdvds1  12104  nprm  12136  dvdsprm  12150  coprm  12157  sqrt2irr  12175  pcmpt  12354  pcmptdvds  12356  pcfac  12361  prmpwdvds  12366  lidrididd  12819  dfgrp2  12923  grpidinv2  12954  dfgrp3mlem  12994  issubg4m  13084  srgrz  13231  srglz  13232  srgisid  13233  islmodd  13477  rmodislmod  13535  rnglidlmcl  13664  cnpnei  13990  lmss  14017  txlm  14050  psmet0  14098  metss  14265  metcnp3  14282  mulc1cncf  14347  cncfco  14349  2sqlem6  14738  2sqlem10  14743  bj-indsuc  14951  bj-inf2vnlem2  14994  trirec0  15064  iswomni0  15071  neap0mkv  15089