Theorem resmptd 5875

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

Syntax hints:   → wi 4   = wceq 1538   ⊆ wss 3881   ↦ cmpt 5110   ↾ cres 5521

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pr 5295

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-rab 3115  df-v 3443  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-sn 4526  df-pr 4528  df-op 4532  df-opab 5093  df-mpt 5111  df-xp 5525  df-rel 5526  df-res 5531

This theorem is referenced by:  f1ossf1o  6867  oacomf1olem  8173  cantnfres  9124  rlimres2  14910  lo1res2  14911  o1res2  14912  fsumss  15074  fprodss  15294  conjsubgen  18383  gsumsplit2  19042  gsum2d  19085  dmdprdsplitlem  19152  dprd2dlem1  19156  psrlidm  20641  psrridm  20642  mplmonmul  20704  mplcoe1  20705  mplcoe5  20708  evlsval2  20759  mdetunilem9  21225  cmpfi  22013  ptpjopn  22217  xkoptsub  22259  xkopjcn  22261  cnmpt1res  22281  subgntr  22712  opnsubg  22713  clsnsg  22715  snclseqg  22721  tsmsxplem1  22758  imasdsf1olem  22980  subgnm  23239  cphsscph  23855  mbfss  24250  mbflimsup  24270  mbfmullem2  24328  iblss  24408  limcres  24489  dvmptresicc  24519  dvaddbr  24541  dvmulbr  24542  dvcmulf  24548  dvmptres3  24559  dvmptres2  24565  dvmptntr  24574  lhop2  24618  lhop  24619  dvfsumle  24624  dvfsumabs  24626  dvfsumlem2  24630  ftc2ditglem  24648  itgsubstlem  24651  itgpowd  24653  mdegfval  24663  psercn2  25018  psercn  25021  abelth  25036  abelth2  25037  efrlim  25555  jensenlem2  25573  lgamcvg2  25640  pntrsumo1  26149  clwlknf1oclwwlknlem3  27868  eucrct2eupth  28030  rabfodom  30274  fmptssfisupp  30445  elrspunidl  31014  poimirlem16  35073  poimirlem19  35076  poimirlem30  35087  ftc1anclem8  35137  ftc2nc  35139  areacirclem2  35146  hbtlem6  40073  radcnvrat  41018  disjf1o  41818  cncfmptss  42229  limsupvaluzmpt  42359  supcnvlimsupmpt  42383  dvnprodlem1  42588  iblsplit  42608  itgcoscmulx  42611  itgiccshift  42622  itgperiod  42623  itgsbtaddcnst  42624  dirkercncflem2  42746  dirkercncflem4  42748  fourierdlem28  42777  fourierdlem40  42789  fourierdlem58  42806  fourierdlem74  42822  fourierdlem75  42823  fourierdlem76  42824  fourierdlem78  42826  fourierdlem80  42828  fourierdlem81  42829  fourierdlem84  42832  fourierdlem85  42833  fourierdlem90  42838  fourierdlem93  42841  fourierdlem101  42849  fourierdlem111  42859  sge0lessmpt  43038  sge0gerpmpt  43041  sge0resrnlem  43042  sge0ssrempt  43044  sge0ltfirpmpt  43047  sge0iunmptlemre  43054  sge0lefimpt  43062  sge0ltfirpmpt2  43065  sge0pnffigtmpt  43079  ismeannd  43106  omeiunltfirp  43158  caratheodorylem2  43166  sssmfmpt  43384  gsumsplit2f  44440  funcrngcsetc  44622  funcrngcsetcALT  44623  funcringcsetc  44659  fdmdifeqresdif  44743