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

Theorem resmptd 5907
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 5904 . 2 (𝐵𝐴 → ((𝑥𝐴𝐶) ↾ 𝐵) = (𝑥𝐵𝐶))
31, 2syl 17 1 (𝜑 → ((𝑥𝐴𝐶) ↾ 𝐵) = (𝑥𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1530  wss 3940  cmpt 5143  cres 5556
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798  ax-sep 5200  ax-nul 5207  ax-pr 5326
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-rab 3152  df-v 3502  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-nul 4296  df-if 4471  df-sn 4565  df-pr 4567  df-op 4571  df-opab 5126  df-mpt 5144  df-xp 5560  df-rel 5561  df-res 5566
This theorem is referenced by:  f1ossf1o  6888  oacomf1olem  8185  cantnfres  9134  rlimres2  14913  lo1res2  14914  o1res2  14915  fsumss  15077  fprodss  15297  conjsubgen  18336  gsumsplit2  18985  gsum2d  19028  dmdprdsplitlem  19095  dprd2dlem1  19099  psrlidm  20118  psrridm  20119  mplmonmul  20180  mplcoe1  20181  mplcoe5  20184  evlsval2  20235  mdetunilem9  21164  cmpfi  21951  ptpjopn  22155  xkoptsub  22197  xkopjcn  22199  cnmpt1res  22219  subgntr  22649  opnsubg  22650  clsnsg  22652  snclseqg  22658  tsmsxplem1  22695  imasdsf1olem  22917  subgnm  23176  cphsscph  23788  mbfss  24181  mbflimsup  24201  mbfmullem2  24259  iblss  24339  limcres  24418  dvaddbr  24469  dvmulbr  24470  dvcmulf  24476  dvmptres3  24487  dvmptres2  24493  dvmptntr  24502  lhop2  24546  lhop  24547  dvfsumle  24552  dvfsumabs  24554  dvfsumlem2  24558  ftc2ditglem  24576  itgsubstlem  24579  mdegfval  24590  psercn2  24945  psercn  24948  abelth  24963  abelth2  24964  efrlim  25480  jensenlem2  25498  lgamcvg2  25565  pntrsumo1  26074  clwlknf1oclwwlknlem3  27795  eucrct2eupth  27957  rabfodom  30199  poimirlem16  34794  poimirlem19  34797  poimirlem30  34808  ftc1anclem8  34860  ftc2nc  34862  areacirclem2  34869  hbtlem6  39613  itgpowd  39705  radcnvrat  40530  disjf1o  41336  cncfmptss  41752  limsupvaluzmpt  41882  supcnvlimsupmpt  41906  dvmptresicc  42088  dvnprodlem1  42115  iblsplit  42135  itgcoscmulx  42138  itgiccshift  42149  itgperiod  42150  itgsbtaddcnst  42151  dirkercncflem2  42274  dirkercncflem4  42276  fourierdlem28  42305  fourierdlem40  42317  fourierdlem58  42334  fourierdlem74  42350  fourierdlem75  42351  fourierdlem76  42352  fourierdlem78  42354  fourierdlem80  42356  fourierdlem81  42357  fourierdlem84  42360  fourierdlem85  42361  fourierdlem90  42366  fourierdlem93  42369  fourierdlem101  42377  fourierdlem111  42387  sge0lessmpt  42566  sge0gerpmpt  42569  sge0resrnlem  42570  sge0ssrempt  42572  sge0ltfirpmpt  42575  sge0iunmptlemre  42582  sge0lefimpt  42590  sge0ltfirpmpt2  42593  sge0pnffigtmpt  42607  ismeannd  42634  omeiunltfirp  42686  caratheodorylem2  42694  sssmfmpt  42912  gsumsplit2f  43938  funcrngcsetc  44171  funcrngcsetcALT  44172  funcringcsetc  44208  fdmdifeqresdif  44292
  Copyright terms: Public domain W3C validator