Theorem rspcv 2919

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

Syntax hints:   -> wi 4   <-> wb 105   = wceq 1398   e. wcel 2205   A.wral 2522

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-ral 2527  df-v 2817

This theorem is referenced by:  rspccv  2920  rspcva  2921  rspccva  2922  rspcdva  2928  rspc3v  2940  rr19.3v  2959  rr19.28v  2960  rspsbc  3129  rspc2vd  3210  intmin  3974  ralxfrALT  4593  ontr2exmid  4652  reg2exmidlema  4661  0elsucexmid  4692  funcnvuni  5430  acexmidlemcase  6053  suppfnss  6470  tfrlem1  6552  tfrlem9  6563  oawordriexmid  6716  nneneq  7124  diffitest  7157  xpfi  7205  ordiso2  7339  exmidontriimlem3  7543  prnmaxl  7819  prnminu  7820  cauappcvgprlemm  7976  cauappcvgprlemladdru  7987  cauappcvgprlemladdrl  7988  caucvgsrlemcl  8120  caucvgsrlemfv  8122  caucvgsr  8133  axcaucvglemres  8230  lbreu  9236  nnsub  9293  supinfneg  9945  infsupneg  9946  ublbneg  9963  fzrevral  10461  zsupcllemex  10612  seq3caopr3  10877  seq3id3  10910  ccatalpha  11326  wrdind  11439  wrd2ind  11440  reuccatpfxs1lem  11463  recan  11819  cau3lem  11824  caubnd2  11827  climshftlemg  12012  subcn2  12021  climcau  12057  serf0  12062  sumdc  12068  isumrpcl  12205  clim2prod  12250  prodmodclem2  12288  ndvdssub  12641  dfgcd3  12731  dfgcd2  12735  coprmgcdb  12810  coprmdvds1  12813  nprm  12845  dvdsprm  12859  coprm  12866  sqrt2irr  12884  pcmpt  13066  pcmptdvds  13068  pcfac  13073  prmpwdvds  13078  lidrididd  13645  dfgrp2  13782  grpidinv2  13813  dfgrp3mlem  13853  issubg4m  13946  srgrz  14227  srglz  14228  srgisid  14229  rrgeq0i  14510  islmodd  14567  rmodislmod  14625  rnglidlmcl  14754  cnpnei  15210  lmss  15237  txlm  15270  psmet0  15318  metss  15485  metcnp3  15502  mulc1cncf  15580  cncfco  15582  2sqlem6  16119  2sqlem10  16124  usgruspgrben  16307  wlk1walkdom  16480  wlkres  16500  clwwlkccatlem  16521  clwwlkext2edg  16543  bj-indsuc  16824  bj-inf2vnlem2  16867  pw1dceq  16904  trirec0  16954  iswomni0  16962  neap0mkv  16981