Theorem resmptd 6041

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

Step	Hyp	Ref	Expression
1		resmptd.b	. 2 ⊢ (𝜑 → 𝐵 ⊆ 𝐴)
2		resmpt 6038	. 2 ⊢ (𝐵 ⊆ 𝐴 → ((𝑥 ∈ 𝐴 ↦ 𝐶) ↾ 𝐵) = (𝑥 ∈ 𝐵 ↦ 𝐶))
3	1, 2	syl 17	1 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐶) ↾ 𝐵) = (𝑥 ∈ 𝐵 ↦ 𝐶))

Syntax hints:   → wi 4   = wceq 1542   ⊆ wss 3949   ↦ cmpt 5232   ↾ cres 5679

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-opab 5212  df-mpt 5233  df-xp 5683  df-rel 5684  df-res 5689

This theorem is referenced by:  f1ossf1o  7126  oacomf1olem  8564  fmptssfisupp  9389  cantnfres  9672  rlimres2  15505  lo1res2  15506  o1res2  15507  fsumss  15671  fprodss  15892  conjsubgen  19125  gsumsplit2  19797  gsum2d  19840  dmdprdsplitlem  19907  dprd2dlem1  19911  psrlidm  21523  psrridm  21524  mplmonmul  21591  mplcoe1  21592  mplcoe5  21595  evlsval2  21650  mdetunilem9  22122  cmpfi  22912  ptpjopn  23116  xkoptsub  23158  xkopjcn  23160  cnmpt1res  23180  subgntr  23611  opnsubg  23612  clsnsg  23614  snclseqg  23620  tsmsxplem1  23657  imasdsf1olem  23879  subgnm  24142  cphsscph  24768  mbfss  25163  mbflimsup  25183  mbfmullem2  25242  iblss  25322  limcres  25403  dvmptresicc  25433  dvaddbr  25455  dvmulbr  25456  dvcmulf  25462  dvmptres3  25473  dvmptres2  25479  dvmptntr  25488  lhop2  25532  lhop  25533  dvfsumle  25538  dvfsumabs  25540  dvfsumlem2  25544  ftc2ditglem  25562  itgsubstlem  25565  itgpowd  25567  mdegfval  25580  psercn2  25935  psercn  25938  abelth  25953  abelth2  25954  efrlim  26474  jensenlem2  26492  lgamcvg2  26559  pntrsumo1  27068  clwlknf1oclwwlknlem3  29336  eucrct2eupth  29498  rabfodom  31743  qusima  32519  elrspunidl  32546  gg-dvmulbr  35175  gg-psercn2  35178  gg-dvfsumle  35182  gg-dvfsumlem2  35183  poimirlem16  36504  poimirlem19  36507  poimirlem30  36518  ftc1anclem8  36568  ftc2nc  36570  areacirclem2  36577  aks4d1p1p5  40940  evlsval3  41131  selvvvval  41157  evlselv  41159  evlsmhpvvval  41167  hbtlem6  41871  radcnvrat  43073  disjf1o  43889  cncfmptss  44303  limsupvaluzmpt  44433  supcnvlimsupmpt  44457  dvnprodlem1  44662  iblsplit  44682  itgcoscmulx  44685  itgiccshift  44696  itgperiod  44697  itgsbtaddcnst  44698  dirkercncflem2  44820  dirkercncflem4  44822  fourierdlem28  44851  fourierdlem40  44863  fourierdlem58  44880  fourierdlem74  44896  fourierdlem75  44897  fourierdlem76  44898  fourierdlem78  44900  fourierdlem80  44902  fourierdlem81  44903  fourierdlem84  44906  fourierdlem85  44907  fourierdlem90  44912  fourierdlem93  44915  fourierdlem101  44923  fourierdlem111  44933  sge0lessmpt  45115  sge0gerpmpt  45118  sge0resrnlem  45119  sge0ssrempt  45121  sge0ltfirpmpt  45124  sge0iunmptlemre  45131  sge0lefimpt  45139  sge0ltfirpmpt2  45142  sge0pnffigtmpt  45156  ismeannd  45183  omeiunltfirp  45235  caratheodorylem2  45243  sssmfmpt  45466  gsumsplit2f  46590  funcrngcsetc  46896  funcrngcsetcALT  46897  funcringcsetc  46933  fdmdifeqresdif  47017