Theorem rspcv 2861

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

Syntax hints:   -> wi 4   <-> wb 105   = wceq 1364   e. wcel 2164   A.wral 2472

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ral 2477  df-v 2762

This theorem is referenced by:  rspccv  2862  rspcva  2863  rspccva  2864  rspcdva  2870  rspc3v  2881  rr19.3v  2900  rr19.28v  2901  rspsbc  3069  rspc2vd  3150  intmin  3891  ralxfrALT  4499  ontr2exmid  4558  reg2exmidlema  4567  0elsucexmid  4598  funcnvuni  5324  acexmidlemcase  5914  tfrlem1  6363  tfrlem9  6374  oawordriexmid  6525  nneneq  6915  diffitest  6945  xpfi  6988  ordiso2  7096  exmidontriimlem3  7285  prnmaxl  7550  prnminu  7551  cauappcvgprlemm  7707  cauappcvgprlemladdru  7718  cauappcvgprlemladdrl  7719  caucvgsrlemcl  7851  caucvgsrlemfv  7853  caucvgsr  7864  axcaucvglemres  7961  lbreu  8966  nnsub  9023  supinfneg  9663  infsupneg  9664  ublbneg  9681  fzrevral  10174  seq3caopr3  10565  seq3id3  10598  recan  11256  cau3lem  11261  caubnd2  11264  climshftlemg  11448  subcn2  11457  climcau  11493  serf0  11498  sumdc  11504  isumrpcl  11640  clim2prod  11685  prodmodclem2  11723  ndvdssub  12074  zsupcllemex  12086  dfgcd3  12150  dfgcd2  12154  coprmgcdb  12229  coprmdvds1  12232  nprm  12264  dvdsprm  12278  coprm  12285  sqrt2irr  12303  pcmpt  12484  pcmptdvds  12486  pcfac  12491  prmpwdvds  12496  lidrididd  12968  dfgrp2  13102  grpidinv2  13133  dfgrp3mlem  13173  issubg4m  13266  srgrz  13483  srglz  13484  srgisid  13485  rrgeq0i  13763  islmodd  13792  rmodislmod  13850  rnglidlmcl  13979  cnpnei  14398  lmss  14425  txlm  14458  psmet0  14506  metss  14673  metcnp3  14690  mulc1cncf  14768  cncfco  14770  2sqlem6  15277  2sqlem10  15282  bj-indsuc  15490  bj-inf2vnlem2  15533  trirec0  15604  iswomni0  15611  neap0mkv  15629