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

Theorem rspcv 2788
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 1509 . 2 𝑥𝜓
2 rspcv.1 . 2 (𝑥 = 𝐴 → (𝜑𝜓))
31, 2rspc 2786 1 (𝐴𝐵 → (∀𝑥𝐵 𝜑𝜓))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104   = wceq 1332  wcel 1481  wral 2417
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122
This theorem depends on definitions:  df-bi 116  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ral 2422  df-v 2691
This theorem is referenced by:  rspccv  2789  rspcva  2790  rspccva  2791  rspcdva  2797  rspc3v  2808  rr19.3v  2826  rr19.28v  2827  rspsbc  2994  intmin  3798  ralxfrALT  4395  ontr2exmid  4447  reg2exmidlema  4456  0elsucexmid  4487  funcnvuni  5199  acexmidlemcase  5776  tfrlem1  6212  tfrlem9  6223  oawordriexmid  6373  nneneq  6758  diffitest  6788  xpfi  6825  ordiso2  6927  prnmaxl  7319  prnminu  7320  cauappcvgprlemm  7476  cauappcvgprlemladdru  7487  cauappcvgprlemladdrl  7488  caucvgsrlemcl  7620  caucvgsrlemfv  7622  caucvgsr  7633  axcaucvglemres  7730  lbreu  8726  nnsub  8782  supinfneg  9416  infsupneg  9417  ublbneg  9431  fzrevral  9915  seq3caopr3  10284  seq3id3  10310  recan  10912  cau3lem  10917  caubnd2  10920  climshftlemg  11102  subcn2  11111  climcau  11147  serf0  11152  sumdc  11158  isumrpcl  11294  clim2prod  11339  prodmodclem2  11377  ndvdssub  11661  zsupcllemex  11673  dfgcd3  11732  dfgcd2  11736  coprmgcdb  11803  coprmdvds1  11806  nprm  11838  dvdsprm  11851  coprm  11856  sqrt2irr  11874  cnpnei  12425  lmss  12452  txlm  12485  psmet0  12533  metss  12700  metcnp3  12717  mulc1cncf  12782  cncfco  12784  bj-indsuc  13295  bj-inf2vnlem2  13338  trirec0  13410
  Copyright terms: Public domain W3C validator