Theorem resmptd 5937

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 5934	. 2 ⊢ (𝐵 ⊆ 𝐴 → ((𝑥 ∈ 𝐴 ↦ 𝐶) ↾ 𝐵) = (𝑥 ∈ 𝐵 ↦ 𝐶))
3	1, 2	syl 17	1 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐶) ↾ 𝐵) = (𝑥 ∈ 𝐵 ↦ 𝐶))

Syntax hints:   → wi 4   = wceq 1539   ⊆ wss 3883   ↦ cmpt 5153   ↾ cres 5582

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-opab 5133  df-mpt 5154  df-xp 5586  df-rel 5587  df-res 5592

This theorem is referenced by:  f1ossf1o  6982  oacomf1olem  8357  cantnfres  9365  rlimres2  15198  lo1res2  15199  o1res2  15200  fsumss  15365  fprodss  15586  conjsubgen  18782  gsumsplit2  19445  gsum2d  19488  dmdprdsplitlem  19555  dprd2dlem1  19559  psrlidm  21082  psrridm  21083  mplmonmul  21147  mplcoe1  21148  mplcoe5  21151  evlsval2  21207  mdetunilem9  21677  cmpfi  22467  ptpjopn  22671  xkoptsub  22713  xkopjcn  22715  cnmpt1res  22735  subgntr  23166  opnsubg  23167  clsnsg  23169  snclseqg  23175  tsmsxplem1  23212  imasdsf1olem  23434  subgnm  23695  cphsscph  24320  mbfss  24715  mbflimsup  24735  mbfmullem2  24794  iblss  24874  limcres  24955  dvmptresicc  24985  dvaddbr  25007  dvmulbr  25008  dvcmulf  25014  dvmptres3  25025  dvmptres2  25031  dvmptntr  25040  lhop2  25084  lhop  25085  dvfsumle  25090  dvfsumabs  25092  dvfsumlem2  25096  ftc2ditglem  25114  itgsubstlem  25117  itgpowd  25119  mdegfval  25132  psercn2  25487  psercn  25490  abelth  25505  abelth2  25506  efrlim  26024  jensenlem2  26042  lgamcvg2  26109  pntrsumo1  26618  clwlknf1oclwwlknlem3  28348  eucrct2eupth  28510  rabfodom  30752  fmptssfisupp  30921  qusima  31496  elrspunidl  31508  poimirlem16  35720  poimirlem19  35723  poimirlem30  35734  ftc1anclem8  35784  ftc2nc  35786  areacirclem2  35793  aks4d1p1p5  40011  evlsval3  40195  evlsbagval  40198  hbtlem6  40870  radcnvrat  41821  disjf1o  42618  cncfmptss  43018  limsupvaluzmpt  43148  supcnvlimsupmpt  43172  dvnprodlem1  43377  iblsplit  43397  itgcoscmulx  43400  itgiccshift  43411  itgperiod  43412  itgsbtaddcnst  43413  dirkercncflem2  43535  dirkercncflem4  43537  fourierdlem28  43566  fourierdlem40  43578  fourierdlem58  43595  fourierdlem74  43611  fourierdlem75  43612  fourierdlem76  43613  fourierdlem78  43615  fourierdlem80  43617  fourierdlem81  43618  fourierdlem84  43621  fourierdlem85  43622  fourierdlem90  43627  fourierdlem93  43630  fourierdlem101  43638  fourierdlem111  43648  sge0lessmpt  43827  sge0gerpmpt  43830  sge0resrnlem  43831  sge0ssrempt  43833  sge0ltfirpmpt  43836  sge0iunmptlemre  43843  sge0lefimpt  43851  sge0ltfirpmpt2  43854  sge0pnffigtmpt  43868  ismeannd  43895  omeiunltfirp  43947  caratheodorylem2  43955  sssmfmpt  44173  gsumsplit2f  45262  funcrngcsetc  45444  funcrngcsetcALT  45445  funcringcsetc  45481  fdmdifeqresdif  45565