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

Theorem resmptd 5593
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 5590 . 2 (𝐵𝐴 → ((𝑥𝐴𝐶) ↾ 𝐵) = (𝑥𝐵𝐶))
31, 2syl 17 1 (𝜑 → ((𝑥𝐴𝐶) ↾ 𝐵) = (𝑥𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1631  wss 3723  cmpt 4863  cres 5251
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4915  ax-nul 4923  ax-pr 5034
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 835  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-rab 3070  df-v 3353  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4226  df-sn 4317  df-pr 4319  df-op 4323  df-opab 4847  df-mpt 4864  df-xp 5255  df-rel 5256  df-res 5261
This theorem is referenced by:  f1ossf1o  6538  oacomf1olem  7798  cantnfres  8738  rlimres2  14500  lo1res2  14501  o1res2  14502  fsumss  14664  fprodss  14885  conjsubgen  17901  gsumsplit2  18536  gsum2d  18578  dmdprdsplitlem  18644  dprd2dlem1  18648  psrlidm  19618  psrridm  19619  mplmonmul  19679  mplcoe1  19680  mplcoe5  19683  evlsval2  19735  mdetunilem9  20644  cmpfi  21432  ptpjopn  21636  xkoptsub  21678  xkopjcn  21680  cnmpt1res  21700  subgntr  22130  opnsubg  22131  clsnsg  22133  snclseqg  22139  tsmsxplem1  22176  imasdsf1olem  22398  subgnm  22657  mbfss  23633  mbflimsup  23653  mbfmullem2  23711  iblss  23791  limcres  23870  dvaddbr  23921  dvmulbr  23922  dvcmulf  23928  dvmptres3  23939  dvmptres2  23945  dvmptntr  23954  lhop2  23998  lhop  23999  dvfsumle  24004  dvfsumabs  24006  dvfsumlem2  24010  ftc2ditglem  24028  itgsubstlem  24031  mdegfval  24042  psercn2  24397  psercn  24400  abelth  24415  abelth2  24416  efrlim  24917  jensenlem2  24935  lgamcvg2  25002  pntrsumo1  25475  eucrct2eupth  27425  clwwlknonclwlknonf1olemOLD  27550  rabfodom  29682  poimirlem16  33758  poimirlem19  33761  poimirlem30  33772  ftc1anclem8  33824  ftc2nc  33826  areacirclem2  33833  hbtlem6  38225  itgpowd  38326  radcnvrat  39039  disjf1o  39898  cncfmptss  40337  limsupvaluzmpt  40467  supcnvlimsupmpt  40491  dvmptresicc  40652  dvnprodlem1  40679  iblsplit  40699  itgcoscmulx  40702  itgiccshift  40713  itgperiod  40714  itgsbtaddcnst  40715  dirkercncflem2  40838  dirkercncflem4  40840  fourierdlem28  40869  fourierdlem40  40881  fourierdlem58  40898  fourierdlem74  40914  fourierdlem75  40915  fourierdlem76  40916  fourierdlem78  40918  fourierdlem80  40920  fourierdlem81  40921  fourierdlem84  40924  fourierdlem85  40925  fourierdlem90  40930  fourierdlem93  40933  fourierdlem101  40941  fourierdlem111  40951  sge0lessmpt  41133  sge0gerpmpt  41136  sge0resrnlem  41137  sge0ssrempt  41139  sge0ltfirpmpt  41142  sge0iunmptlemre  41149  sge0lefimpt  41157  sge0ltfirpmpt2  41160  sge0pnffigtmpt  41174  ismeannd  41201  omeiunltfirp  41253  caratheodorylem2  41261  sssmfmpt  41479  funcrngcsetc  42526  funcrngcsetcALT  42527  funcringcsetc  42563  fdmdifeqresdif  42648  gsumsplit2f  42671
  Copyright terms: Public domain W3C validator