Theorem resmptd 6027

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

Syntax hints:   → wi 4   = wceq 1540   ⊆ wss 3926   ↦ cmpt 5201   ↾ cres 5656

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-opab 5182  df-mpt 5202  df-xp 5660  df-rel 5661  df-res 5666

This theorem is referenced by:  f1ossf1o  7118  oacomf1olem  8576  fmptssfisupp  9406  cantnfres  9691  rlimres2  15577  lo1res2  15578  o1res2  15579  fsumss  15741  fprodss  15964  conjsubgen  19234  gsumsplit2  19910  gsum2d  19953  dmdprdsplitlem  20020  dprd2dlem1  20024  funcrngcsetc  20600  funcrngcsetcALT  20601  funcringcsetc  20634  psrlidm  21922  psrridm  21923  mplmonmul  21994  mplcoe1  21995  mplcoe5  21998  evlsval2  22045  mdetunilem9  22558  cmpfi  23346  ptpjopn  23550  xkoptsub  23592  xkopjcn  23594  cnmpt1res  23614  subgntr  24045  opnsubg  24046  clsnsg  24048  snclseqg  24054  tsmsxplem1  24091  imasdsf1olem  24312  subgnm  24572  cphsscph  25203  mbfss  25599  mbflimsup  25619  mbfmullem2  25677  iblss  25758  limcres  25839  dvmptresicc  25869  dvaddbr  25892  dvmulbr  25893  dvmulbrOLD  25894  dvcmulf  25900  dvmptres3  25912  dvmptres2  25918  dvmptntr  25927  lhop2  25972  lhop  25973  dvfsumle  25978  dvfsumleOLD  25979  dvfsumabs  25981  dvfsumlem2  25985  dvfsumlem2OLD  25986  ftc2ditglem  26004  itgsubstlem  26007  itgpowd  26009  mdegfval  26019  psercn2  26384  psercn2OLD  26385  psercn  26388  abelth  26403  abelth2  26404  efrlim  26931  efrlimOLD  26932  jensenlem2  26950  lgamcvg2  27017  pntrsumo1  27528  clwlknf1oclwwlknlem3  30064  eucrct2eupth  30226  rabfodom  32486  qusima  33423  elrspunidl  33443  ressply1evls1  33578  poimirlem16  37660  poimirlem19  37663  poimirlem30  37674  ftc1anclem8  37724  ftc2nc  37726  areacirclem2  37733  aks4d1p1p5  42088  aks6d1c6lem2  42184  aks6d1c6lem4  42186  evlsval3  42582  selvvvval  42608  evlselv  42610  evlsmhpvvval  42618  hbtlem6  43153  radcnvrat  44338  disjf1o  45215  cncfmptss  45616  limsupvaluzmpt  45746  supcnvlimsupmpt  45770  dvnprodlem1  45975  iblsplit  45995  itgcoscmulx  45998  itgiccshift  46009  itgperiod  46010  itgsbtaddcnst  46011  dirkercncflem2  46133  dirkercncflem4  46135  fourierdlem28  46164  fourierdlem40  46176  fourierdlem58  46193  fourierdlem74  46209  fourierdlem75  46210  fourierdlem76  46211  fourierdlem78  46213  fourierdlem80  46215  fourierdlem81  46216  fourierdlem84  46219  fourierdlem85  46220  fourierdlem90  46225  fourierdlem93  46228  fourierdlem101  46236  fourierdlem111  46246  sge0lessmpt  46428  sge0gerpmpt  46431  sge0resrnlem  46432  sge0ssrempt  46434  sge0ltfirpmpt  46437  sge0iunmptlemre  46444  sge0lefimpt  46452  sge0ltfirpmpt2  46455  sge0pnffigtmpt  46469  ismeannd  46496  omeiunltfirp  46548  caratheodorylem2  46556  sssmfmpt  46779  gsumsplit2f  48155  fdmdifeqresdif  48317