Theorem resmptd 6044

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

Syntax hints:   → wi 4   = wceq 1570   ⊆ wss 3906   ↦ cmpt 5193   ↾ cres 5665

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-12 2213  ax-ext 2735  ax-sep 5258  ax-pr 5406

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-opab 5175  df-mpt 5194  df-xp 5669  df-rel 5670  df-res 5675

This theorem is referenced by:  f1ossf1o  7126  oacomf1olem  8550  fmptssfisupp  9355  cantnfres  9647  rlimres2  15614  lo1res2  15615  o1res2  15616  fsumss  15778  fprodss  16004  conjsubgen  19322  gsumsplit2  20000  gsum2d  20043  dmdprdsplitlem  20110  dprd2dlem1  20114  funcrngcsetc  20726  funcrngcsetcALT  20727  funcringcsetc  20760  psrlidm  22092  psrridm  22093  mplmonmul  22168  mplcoe1  22169  mplcoe5  22172  evlsval2  22219  evlsval3  22221  selvvvval  22274  mdetunilem9  22758  cmpfi  23546  ptpjopn  23750  xkoptsub  23792  xkopjcn  23794  cnmpt1res  23814  subgntr  24245  opnsubg  24246  clsnsg  24248  snclseqg  24254  tsmsxplem1  24291  imasdsf1olem  24511  subgnm  24771  cphsscph  25391  mbfss  25786  mbflimsup  25806  mbfmullem2  25864  iblss  25945  limcres  26026  dvmptresicc  26056  dvaddbr  26078  dvmulbr  26079  dvcmulf  26085  dvmptres3  26096  dvmptres2  26102  dvmptntr  26111  lhop2  26155  lhop  26156  dvfsumle  26161  dvfsumabs  26163  dvfsumlem2  26167  ftc2ditglem  26185  itgsubstlem  26188  itgpowd  26190  mdegfval  26200  psercn2  26564  psercn  26567  abelth  26582  abelth2  26583  efrlim  27112  jensenlem2  27130  lgamcvg2  27197  pntrsumo1  27707  clwlknf1oclwwlknlem3  30412  eucrct2eupth  30574  rabfodom  32829  gsummptfsres  33352  qusima  33695  elrspunidl  33714  ressply1evls1  33833  psrmonmul  33918  poimirlem16  38265  poimirlem19  38268  poimirlem30  38279  ftc1anclem8  38329  ftc2nc  38331  areacirclem2  38338  aks4d1p1p5  42820  aks6d1c6lem2  42916  aks6d1c6lem4  42918  evlselv  43301  evlsmhpvvval  43307  hbtlem6  43836  radcnvrat  45004  disjf1o  45889  cncfmptss  46283  limsupvaluzmpt  46411  supcnvlimsupmpt  46435  dvnprodlem1  46640  iblsplit  46660  itgcoscmulx  46663  itgiccshift  46674  itgperiod  46675  itgsbtaddcnst  46676  dirkercncflem2  46798  dirkercncflem4  46800  fourierdlem28  46829  fourierdlem40  46841  fourierdlem58  46858  fourierdlem74  46874  fourierdlem75  46875  fourierdlem76  46876  fourierdlem78  46878  fourierdlem80  46880  fourierdlem81  46881  fourierdlem84  46884  fourierdlem85  46885  fourierdlem90  46890  fourierdlem93  46893  fourierdlem101  46901  fourierdlem111  46911  sge0lessmpt  47093  sge0gerpmpt  47096  sge0resrnlem  47097  sge0ssrempt  47099  sge0ltfirpmpt  47102  sge0iunmptlemre  47109  sge0lefimpt  47117  sge0ltfirpmpt2  47120  sge0pnffigtmpt  47134  ismeannd  47161  omeiunltfirp  47213  caratheodorylem2  47221  sssmfmpt  47444  gsumsplit2f  48922  fdmdifeqresdif  49099