Theorem rspcv 2652

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

Syntax hints:   -> wi 4   <-> wb 98   = wceq 1243   e. wcel 1393   A.wral 2306

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022

This theorem depends on definitions:  df-bi 110  df-tru 1246  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-ral 2311  df-v 2559

This theorem is referenced by:  rspccv  2653  rspcva  2654  rspccva  2655  rspc3v  2665  rr19.3v  2682  rr19.28v  2683  rspsbc  2840  intmin  3635  frirrg  4087  ralxfrALT  4199  ontr2exmid  4250  reg2exmidlema  4259  0elsucexmid  4289  wetriext  4301  funcnvuni  4968  acexmidlemcase  5507  grprinvlem  5695  grprinvd  5696  caofref  5732  tfrlem1  5923  tfrlem5  5930  tfrlem9  5935  rdgon  5973  nneneq  6320  diffitest  6344  ordiso2  6357  prltlu  6585  prnmaxl  6586  prnminu  6587  cauappcvgprlemm  6743  cauappcvgprlemladdru  6754  cauappcvgprlemladdrl  6755  caucvgprlemm  6766  caucvgprprlemml  6792  caucvgsrlemcl  6873  caucvgsrlemfv  6875  caucvgsr  6886  axcaucvglemres  6973  nnsub  7952  ublbneg  8548  fzrevral  8967  iseqovex  9219  iseqval  9220  iseqfn  9221  iseq1  9222  iseqcl  9223  iseqp1  9225  iseqfveq2  9228  iseqfveq  9230  iseqfeq  9231  iseqshft2  9232  monoord  9235  monoord2  9236  isermono  9237  iseqsplit  9238  iseqcaopr3  9240  iseqid3s  9246  iseqid  9247  iseqhomo  9248  cvg1nlemcau  9583  cvg1nlemres  9584  recvguniq  9593  resqrexlemgt0  9618  resqrexlemoverl  9619  resqrexlemglsq  9620  recan  9705  cau3lem  9710  caubnd2  9713  climi  9808  climshftlemg  9823  climcn1  9829  subcn2  9832  climcau  9866  serif0  9871  sqrt2irr  9878  bj-indsuc  10052  bj-inf2vnlem2  10096