Theorem resmptd 6038

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

Syntax hints:   → wi 4   = wceq 1541   ⊆ wss 3947   ↦ cmpt 5230   ↾ cres 5677

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-12 2171  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pr 5426

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-opab 5210  df-mpt 5231  df-xp 5681  df-rel 5682  df-res 5687

This theorem is referenced by:  f1ossf1o  7122  oacomf1olem  8560  fmptssfisupp  9385  cantnfres  9668  rlimres2  15501  lo1res2  15502  o1res2  15503  fsumss  15667  fprodss  15888  conjsubgen  19119  gsumsplit2  19791  gsum2d  19834  dmdprdsplitlem  19901  dprd2dlem1  19905  psrlidm  21514  psrridm  21515  mplmonmul  21582  mplcoe1  21583  mplcoe5  21586  evlsval2  21641  mdetunilem9  22113  cmpfi  22903  ptpjopn  23107  xkoptsub  23149  xkopjcn  23151  cnmpt1res  23171  subgntr  23602  opnsubg  23603  clsnsg  23605  snclseqg  23611  tsmsxplem1  23648  imasdsf1olem  23870  subgnm  24133  cphsscph  24759  mbfss  25154  mbflimsup  25174  mbfmullem2  25233  iblss  25313  limcres  25394  dvmptresicc  25424  dvaddbr  25446  dvmulbr  25447  dvcmulf  25453  dvmptres3  25464  dvmptres2  25470  dvmptntr  25479  lhop2  25523  lhop  25524  dvfsumle  25529  dvfsumabs  25531  dvfsumlem2  25535  ftc2ditglem  25553  itgsubstlem  25556  itgpowd  25558  mdegfval  25571  psercn2  25926  psercn  25929  abelth  25944  abelth2  25945  efrlim  26463  jensenlem2  26481  lgamcvg2  26548  pntrsumo1  27057  clwlknf1oclwwlknlem3  29325  eucrct2eupth  29487  rabfodom  31730  qusima  32507  elrspunidl  32534  gg-dvmulbr  35163  gg-psercn2  35166  gg-dvfsumle  35170  gg-dvfsumlem2  35171  poimirlem16  36492  poimirlem19  36495  poimirlem30  36506  ftc1anclem8  36556  ftc2nc  36558  areacirclem2  36565  aks4d1p1p5  40928  evlsval3  41128  selvvvval  41154  evlselv  41156  evlsmhpvvval  41164  hbtlem6  41856  radcnvrat  43058  disjf1o  43874  cncfmptss  44289  limsupvaluzmpt  44419  supcnvlimsupmpt  44443  dvnprodlem1  44648  iblsplit  44668  itgcoscmulx  44671  itgiccshift  44682  itgperiod  44683  itgsbtaddcnst  44684  dirkercncflem2  44806  dirkercncflem4  44808  fourierdlem28  44837  fourierdlem40  44849  fourierdlem58  44866  fourierdlem74  44882  fourierdlem75  44883  fourierdlem76  44884  fourierdlem78  44886  fourierdlem80  44888  fourierdlem81  44889  fourierdlem84  44892  fourierdlem85  44893  fourierdlem90  44898  fourierdlem93  44901  fourierdlem101  44909  fourierdlem111  44919  sge0lessmpt  45101  sge0gerpmpt  45104  sge0resrnlem  45105  sge0ssrempt  45107  sge0ltfirpmpt  45110  sge0iunmptlemre  45117  sge0lefimpt  45125  sge0ltfirpmpt2  45128  sge0pnffigtmpt  45142  ismeannd  45169  omeiunltfirp  45221  caratheodorylem2  45229  sssmfmpt  45452  gsumsplit2f  46576  funcrngcsetc  46849  funcrngcsetcALT  46850  funcringcsetc  46886  fdmdifeqresdif  46970