Theorem resmptd 5993

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

Syntax hints:   → wi 4   = wceq 1541   ⊆ wss 3898   ↦ cmpt 5174   ↾ cres 5621

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-12 2182  ax-ext 2705  ax-sep 5236  ax-nul 5246  ax-pr 5372

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-opab 5156  df-mpt 5175  df-xp 5625  df-rel 5626  df-res 5631

This theorem is referenced by:  f1ossf1o  7067  oacomf1olem  8485  fmptssfisupp  9285  cantnfres  9574  rlimres2  15470  lo1res2  15471  o1res2  15472  fsumss  15634  fprodss  15857  conjsubgen  19165  gsumsplit2  19843  gsum2d  19886  dmdprdsplitlem  19953  dprd2dlem1  19957  funcrngcsetc  20557  funcrngcsetcALT  20558  funcringcsetc  20591  psrlidm  21900  psrridm  21901  mplmonmul  21972  mplcoe1  21973  mplcoe5  21976  evlsval2  22023  mdetunilem9  22536  cmpfi  23324  ptpjopn  23528  xkoptsub  23570  xkopjcn  23572  cnmpt1res  23592  subgntr  24023  opnsubg  24024  clsnsg  24026  snclseqg  24032  tsmsxplem1  24069  imasdsf1olem  24289  subgnm  24549  cphsscph  25179  mbfss  25575  mbflimsup  25595  mbfmullem2  25653  iblss  25734  limcres  25815  dvmptresicc  25845  dvaddbr  25868  dvmulbr  25869  dvmulbrOLD  25870  dvcmulf  25876  dvmptres3  25888  dvmptres2  25894  dvmptntr  25903  lhop2  25948  lhop  25949  dvfsumle  25954  dvfsumleOLD  25955  dvfsumabs  25957  dvfsumlem2  25961  dvfsumlem2OLD  25962  ftc2ditglem  25980  itgsubstlem  25983  itgpowd  25985  mdegfval  25995  psercn2  26360  psercn2OLD  26361  psercn  26364  abelth  26379  abelth2  26380  efrlim  26907  efrlimOLD  26908  jensenlem2  26926  lgamcvg2  26993  pntrsumo1  27504  clwlknf1oclwwlknlem3  30065  eucrct2eupth  30227  rabfodom  32487  qusima  33380  elrspunidl  33400  ressply1evls1  33535  poimirlem16  37697  poimirlem19  37700  poimirlem30  37711  ftc1anclem8  37761  ftc2nc  37763  areacirclem2  37770  aks4d1p1p5  42189  aks6d1c6lem2  42285  aks6d1c6lem4  42287  evlsval3  42678  selvvvval  42704  evlselv  42706  evlsmhpvvval  42714  hbtlem6  43247  radcnvrat  44432  disjf1o  45313  cncfmptss  45712  limsupvaluzmpt  45840  supcnvlimsupmpt  45864  dvnprodlem1  46069  iblsplit  46089  itgcoscmulx  46092  itgiccshift  46103  itgperiod  46104  itgsbtaddcnst  46105  dirkercncflem2  46227  dirkercncflem4  46229  fourierdlem28  46258  fourierdlem40  46270  fourierdlem58  46287  fourierdlem74  46303  fourierdlem75  46304  fourierdlem76  46305  fourierdlem78  46307  fourierdlem80  46309  fourierdlem81  46310  fourierdlem84  46313  fourierdlem85  46314  fourierdlem90  46319  fourierdlem93  46322  fourierdlem101  46330  fourierdlem111  46340  sge0lessmpt  46522  sge0gerpmpt  46525  sge0resrnlem  46526  sge0ssrempt  46528  sge0ltfirpmpt  46531  sge0iunmptlemre  46538  sge0lefimpt  46546  sge0ltfirpmpt2  46549  sge0pnffigtmpt  46563  ismeannd  46590  omeiunltfirp  46642  caratheodorylem2  46650  sssmfmpt  46873  gsumsplit2f  48305  fdmdifeqresdif  48467