Theorem resmptd 5999

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

Syntax hints:   → wi 4   = wceq 1542   ⊆ wss 3890   ↦ cmpt 5167   ↾ cres 5626

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-pr 5370

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-opab 5149  df-mpt 5168  df-xp 5630  df-rel 5631  df-res 5636

This theorem is referenced by:  f1ossf1o  7075  oacomf1olem  8492  fmptssfisupp  9300  cantnfres  9589  rlimres2  15514  lo1res2  15515  o1res2  15516  fsumss  15678  fprodss  15904  conjsubgen  19217  gsumsplit2  19895  gsum2d  19938  dmdprdsplitlem  20005  dprd2dlem1  20009  funcrngcsetc  20608  funcrngcsetcALT  20609  funcringcsetc  20642  psrlidm  21950  psrridm  21951  mplmonmul  22024  mplcoe1  22025  mplcoe5  22028  evlsval2  22075  evlsval3  22077  mdetunilem9  22595  cmpfi  23383  ptpjopn  23587  xkoptsub  23629  xkopjcn  23631  cnmpt1res  23651  subgntr  24082  opnsubg  24083  clsnsg  24085  snclseqg  24091  tsmsxplem1  24128  imasdsf1olem  24348  subgnm  24608  cphsscph  25228  mbfss  25623  mbflimsup  25643  mbfmullem2  25701  iblss  25782  limcres  25863  dvmptresicc  25893  dvaddbr  25915  dvmulbr  25916  dvcmulf  25922  dvmptres3  25933  dvmptres2  25939  dvmptntr  25948  lhop2  25992  lhop  25993  dvfsumle  25998  dvfsumabs  26000  dvfsumlem2  26004  ftc2ditglem  26022  itgsubstlem  26025  itgpowd  26027  mdegfval  26037  psercn2  26401  psercn  26404  abelth  26419  abelth2  26420  efrlim  26946  efrlimOLD  26947  jensenlem2  26965  lgamcvg2  27032  pntrsumo1  27542  clwlknf1oclwwlknlem3  30168  eucrct2eupth  30330  rabfodom  32590  gsummptfsres  33130  qusima  33483  elrspunidl  33503  ressply1evls1  33640  psrmonmul  33709  poimirlem16  37971  poimirlem19  37974  poimirlem30  37985  ftc1anclem8  38035  ftc2nc  38037  areacirclem2  38044  aks4d1p1p5  42528  aks6d1c6lem2  42624  aks6d1c6lem4  42626  selvvvval  43032  evlselv  43034  evlsmhpvvval  43042  hbtlem6  43575  radcnvrat  44759  disjf1o  45639  cncfmptss  46035  limsupvaluzmpt  46163  supcnvlimsupmpt  46187  dvnprodlem1  46392  iblsplit  46412  itgcoscmulx  46415  itgiccshift  46426  itgperiod  46427  itgsbtaddcnst  46428  dirkercncflem2  46550  dirkercncflem4  46552  fourierdlem28  46581  fourierdlem40  46593  fourierdlem58  46610  fourierdlem74  46626  fourierdlem75  46627  fourierdlem76  46628  fourierdlem78  46630  fourierdlem80  46632  fourierdlem81  46633  fourierdlem84  46636  fourierdlem85  46637  fourierdlem90  46642  fourierdlem93  46645  fourierdlem101  46653  fourierdlem111  46663  sge0lessmpt  46845  sge0gerpmpt  46848  sge0resrnlem  46849  sge0ssrempt  46851  sge0ltfirpmpt  46854  sge0iunmptlemre  46861  sge0lefimpt  46869  sge0ltfirpmpt2  46872  sge0pnffigtmpt  46886  ismeannd  46913  omeiunltfirp  46965  caratheodorylem2  46973  sssmfmpt  47196  gsumsplit2f  48668  fdmdifeqresdif  48830