ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  rspcv GIF version

Theorem rspcv 2652
Description: Restricted specialization, using implicit substitution. (Contributed by NM, 26-May-1998.)
Hypothesis
Ref Expression
rspcv.1 (𝑥 = 𝐴 → (𝜑𝜓))
Assertion
Ref Expression
rspcv (𝐴𝐵 → (∀𝑥𝐵 𝜑𝜓))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝜓,𝑥
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem rspcv
StepHypRef Expression
1 nfv 1421 . 2 𝑥𝜓
2 rspcv.1 . 2 (𝑥 = 𝐴 → (𝜑𝜓))
31, 2rspc 2650 1 (𝐴𝐵 → (∀𝑥𝐵 𝜑𝜓))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 98   = wceq 1243  wcel 1393  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  6355  prltlu  6583  prnmaxl  6584  prnminu  6585  cauappcvgprlemm  6741  cauappcvgprlemladdru  6752  cauappcvgprlemladdrl  6753  caucvgprlemm  6764  caucvgprprlemml  6790  caucvgsrlemcl  6871  caucvgsrlemfv  6873  caucvgsr  6884  axcaucvglemres  6971  nnsub  7950  ublbneg  8546  fzrevral  8965  iseqovex  9193  iseqval  9194  iseqfn  9195  iseq1  9196  iseqcl  9197  iseqp1  9199  iseqfveq2  9202  iseqfveq  9204  iseqfeq  9205  iseqshft2  9206  monoord  9209  monoord2  9210  isermono  9211  iseqsplit  9212  iseqcaopr3  9214  iseqid3s  9220  iseqid  9221  iseqhomo  9222  cvg1nlemcau  9557  cvg1nlemres  9558  recvguniq  9567  resqrexlemgt0  9592  resqrexlemoverl  9593  resqrexlemglsq  9594  recan  9679  cau3lem  9684  caubnd2  9687  climi  9782  climshftlemg  9797  climcn1  9803  subcn2  9806  climcau  9840  serif0  9845  sqrt2irr  9852  bj-indsuc  10026  bj-inf2vnlem2  10070
  Copyright terms: Public domain W3C validator