MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  resmptd Structured version   Visualization version   GIF version

Theorem resmptd 5415
Description: Restriction of the mapping operation, deduction form. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypothesis
Ref Expression
resmptd.b (𝜑𝐵𝐴)
Assertion
Ref Expression
resmptd (𝜑 → ((𝑥𝐴𝐶) ↾ 𝐵) = (𝑥𝐵𝐶))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵
Allowed substitution hints:   𝜑(𝑥)   𝐶(𝑥)

Proof of Theorem resmptd
StepHypRef Expression
1 resmptd.b . 2 (𝜑𝐵𝐴)
2 resmpt 5412 . 2 (𝐵𝐴 → ((𝑥𝐴𝐶) ↾ 𝐵) = (𝑥𝐵𝐶))
31, 2syl 17 1 (𝜑 → ((𝑥𝐴𝐶) ↾ 𝐵) = (𝑥𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1480  wss 3560  cmpt 4678  cres 5081
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606  ax-sep 4746  ax-nul 4754  ax-pr 4872
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-clab 2613  df-cleq 2619  df-clel 2622  df-nfc 2756  df-rab 2921  df-v 3193  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-nul 3897  df-if 4064  df-sn 4154  df-pr 4156  df-op 4160  df-opab 4679  df-mpt 4680  df-xp 5085  df-rel 5086  df-res 5091
This theorem is referenced by:  oacomf1olem  7590  cantnfres  8519  rlimres2  14221  lo1res2  14222  o1res2  14223  fsumss  14384  fprodss  14598  conjsubgen  17609  gsumsplit2  18245  gsum2d  18287  dmdprdsplitlem  18352  dprd2dlem1  18356  psrlidm  19317  psrridm  19318  mplmonmul  19378  mplcoe1  19379  mplcoe5  19382  evlsval2  19434  mdetunilem9  20340  cmpfi  21116  ptpjopn  21320  xkoptsub  21362  xkopjcn  21364  cnmpt1res  21384  subgntr  21815  opnsubg  21816  clsnsg  21818  snclseqg  21824  tsmsxplem1  21861  imasdsf1olem  22083  subgnm  22342  mbfss  23314  mbflimsup  23334  mbfmullem2  23392  iblss  23472  limcres  23551  dvaddbr  23602  dvmulbr  23603  dvcmulf  23609  dvmptres3  23620  dvmptres2  23626  dvmptntr  23635  lhop2  23677  lhop  23678  dvfsumle  23683  dvfsumabs  23685  dvfsumlem2  23689  ftc2ditglem  23707  itgsubstlem  23710  mdegfval  23721  psercn2  24076  psercn  24079  abelth  24094  abelth2  24095  efrlim  24591  jensenlem2  24609  lgamcvg2  24676  pntrsumo1  25149  eucrct2eupth  26965  rabfodom  29182  poimirlem16  33043  poimirlem19  33046  poimirlem30  33057  ftc1anclem8  33110  ftc2nc  33112  areacirclem2  33119  hbtlem6  37166  itgpowd  37267  radcnvrat  37981  disjf1o  38838  cncfmptss  39210  limsupvaluzmpt  39340  dvmptresicc  39427  dvnprodlem1  39454  iblsplit  39476  itgcoscmulx  39479  itgiccshift  39490  itgperiod  39491  itgsbtaddcnst  39492  dirkercncflem2  39615  dirkercncflem4  39617  fourierdlem28  39646  fourierdlem40  39658  fourierdlem58  39675  fourierdlem74  39691  fourierdlem75  39692  fourierdlem76  39693  fourierdlem78  39695  fourierdlem80  39697  fourierdlem81  39698  fourierdlem84  39701  fourierdlem85  39702  fourierdlem90  39707  fourierdlem93  39710  fourierdlem101  39718  fourierdlem111  39728  sge0lessmpt  39910  sge0gerpmpt  39913  sge0resrnlem  39914  sge0ssrempt  39916  sge0ltfirpmpt  39919  sge0iunmptlemre  39926  sge0lefimpt  39934  sge0ltfirpmpt2  39937  sge0pnffigtmpt  39951  ismeannd  39978  omeiunltfirp  40027  caratheodorylem2  40035  sssmfmpt  40253  funcrngcsetc  41259  funcrngcsetcALT  41260  funcringcsetc  41296  fdmdifeqresdif  41381  gsumsplit2f  41404
  Copyright terms: Public domain W3C validator