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  4514  ontr2exmid  4573  reg2exmidlema  4582  0elsucexmid  4613  funcnvuni  5343  acexmidlemcase  5939  tfrlem1  6394  tfrlem9  6405  oawordriexmid  6556  nneneq  6954  diffitest  6984  xpfi  7029  ordiso2  7137  exmidontriimlem3  7335  prnmaxl  7601  prnminu  7602  cauappcvgprlemm  7758  cauappcvgprlemladdru  7769  cauappcvgprlemladdrl  7770  caucvgsrlemcl  7902  caucvgsrlemfv  7904  caucvgsr  7915  axcaucvglemres  8012  lbreu  9018  nnsub  9075  supinfneg  9716  infsupneg  9717  ublbneg  9734  fzrevral  10227  zsupcllemex  10373  seq3caopr3  10636  seq3id3  10669  recan  11420  cau3lem  11425  caubnd2  11428  climshftlemg  11613  subcn2  11622  climcau  11658  serf0  11663  sumdc  11669  isumrpcl  11805  clim2prod  11850  prodmodclem2  11888  ndvdssub  12241  dfgcd3  12331  dfgcd2  12335  coprmgcdb  12410  coprmdvds1  12413  nprm  12445  dvdsprm  12459  coprm  12466  sqrt2irr  12484  pcmpt  12666  pcmptdvds  12668  pcfac  12673  prmpwdvds  12678  lidrididd  13214  dfgrp2  13359  grpidinv2  13390  dfgrp3mlem  13430  issubg4m  13529  srgrz  13746  srglz  13747  srgisid  13748  rrgeq0i  14026  islmodd  14055  rmodislmod  14113  rnglidlmcl  14242  cnpnei  14691  lmss  14718  txlm  14751  psmet0  14799  metss  14966  metcnp3  14983  mulc1cncf  15061  cncfco  15063  2sqlem6  15597  2sqlem10  15602  bj-indsuc  15864  bj-inf2vnlem2  15907  trirec0  15983  iswomni0  15990  neap0mkv  16008