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 1547   ⊆ wss 3890   ↦ cmpt 5160   ↾ cres 5627

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-12 2189  ax-ext 2712  ax-sep 5225  ax-pr 5369

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-opab 5142  df-mpt 5161  df-xp 5631  df-rel 5632  df-res 5637

This theorem is referenced by:  f1ossf1o  7077  oacomf1olem  8496  fmptssfisupp  9304  cantnfres  9596  rlimres2  15521  lo1res2  15522  o1res2  15523  fsumss  15685  fprodss  15911  conjsubgen  19224  gsumsplit2  19902  gsum2d  19945  dmdprdsplitlem  20012  dprd2dlem1  20016  funcrngcsetc  20619  funcrngcsetcALT  20620  funcringcsetc  20653  psrlidm  21943  psrridm  21944  mplmonmul  22019  mplcoe1  22020  mplcoe5  22023  evlsval2  22070  evlsval3  22072  selvvvval  22125  mdetunilem9  22610  cmpfi  23398  ptpjopn  23602  xkoptsub  23644  xkopjcn  23646  cnmpt1res  23666  subgntr  24097  opnsubg  24098  clsnsg  24100  snclseqg  24106  tsmsxplem1  24143  imasdsf1olem  24363  subgnm  24623  cphsscph  25243  mbfss  25638  mbflimsup  25658  mbfmullem2  25716  iblss  25797  limcres  25878  dvmptresicc  25908  dvaddbr  25930  dvmulbr  25931  dvcmulf  25937  dvmptres3  25948  dvmptres2  25954  dvmptntr  25963  lhop2  26007  lhop  26008  dvfsumle  26013  dvfsumabs  26015  dvfsumlem2  26019  ftc2ditglem  26037  itgsubstlem  26040  itgpowd  26042  mdegfval  26052  psercn2  26413  psercn  26416  abelth  26431  abelth2  26432  efrlim  26958  jensenlem2  26976  lgamcvg2  27043  pntrsumo1  27553  clwlknf1oclwwlknlem3  30178  eucrct2eupth  30340  rabfodom  32600  gsummptfsres  33142  qusima  33498  elrspunidl  33518  ressply1evls1  33655  psrmonmul  33741  poimirlem16  38010  poimirlem19  38013  poimirlem30  38024  ftc1anclem8  38074  ftc2nc  38076  areacirclem2  38083  aks4d1p1p5  42567  aks6d1c6lem2  42663  aks6d1c6lem4  42665  evlselv  43046  evlsmhpvvval  43052  hbtlem6  43581  radcnvrat  44765  disjf1o  45645  cncfmptss  46039  limsupvaluzmpt  46167  supcnvlimsupmpt  46191  dvnprodlem1  46396  iblsplit  46416  itgcoscmulx  46419  itgiccshift  46430  itgperiod  46431  itgsbtaddcnst  46432  dirkercncflem2  46554  dirkercncflem4  46556  fourierdlem28  46585  fourierdlem40  46597  fourierdlem58  46614  fourierdlem74  46630  fourierdlem75  46631  fourierdlem76  46632  fourierdlem78  46634  fourierdlem80  46636  fourierdlem81  46637  fourierdlem84  46640  fourierdlem85  46641  fourierdlem90  46646  fourierdlem93  46649  fourierdlem101  46657  fourierdlem111  46667  sge0lessmpt  46849  sge0gerpmpt  46852  sge0resrnlem  46853  sge0ssrempt  46855  sge0ltfirpmpt  46858  sge0iunmptlemre  46865  sge0lefimpt  46873  sge0ltfirpmpt2  46876  sge0pnffigtmpt  46890  ismeannd  46917  omeiunltfirp  46969  caratheodorylem2  46977  sssmfmpt  47200  gsumsplit2f  48678  fdmdifeqresdif  48840