Theorem resmptd 5882

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

Syntax hints:   → wi 4   = wceq 1542   ⊆ wss 3843   ↦ cmpt 5110   ↾ cres 5527

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 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-10 2145  ax-12 2179  ax-ext 2710  ax-sep 5167  ax-nul 5174  ax-pr 5296

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2075  df-clab 2717  df-cleq 2730  df-clel 2811  df-rab 3062  df-v 3400  df-dif 3846  df-un 3848  df-in 3850  df-ss 3860  df-nul 4212  df-if 4415  df-sn 4517  df-pr 4519  df-op 4523  df-opab 5093  df-mpt 5111  df-xp 5531  df-rel 5532  df-res 5537

This theorem is referenced by:  f1ossf1o  6900  oacomf1olem  8221  cantnfres  9213  rlimres2  15008  lo1res2  15009  o1res2  15010  fsumss  15175  fprodss  15394  conjsubgen  18509  gsumsplit2  19168  gsum2d  19211  dmdprdsplitlem  19278  dprd2dlem1  19282  psrlidm  20782  psrridm  20783  mplmonmul  20847  mplcoe1  20848  mplcoe5  20851  evlsval2  20901  mdetunilem9  21371  cmpfi  22159  ptpjopn  22363  xkoptsub  22405  xkopjcn  22407  cnmpt1res  22427  subgntr  22858  opnsubg  22859  clsnsg  22861  snclseqg  22867  tsmsxplem1  22904  imasdsf1olem  23126  subgnm  23386  cphsscph  24003  mbfss  24398  mbflimsup  24418  mbfmullem2  24477  iblss  24557  limcres  24638  dvmptresicc  24668  dvaddbr  24690  dvmulbr  24691  dvcmulf  24697  dvmptres3  24708  dvmptres2  24714  dvmptntr  24723  lhop2  24767  lhop  24768  dvfsumle  24773  dvfsumabs  24775  dvfsumlem2  24779  ftc2ditglem  24797  itgsubstlem  24800  itgpowd  24802  mdegfval  24815  psercn2  25170  psercn  25173  abelth  25188  abelth2  25189  efrlim  25707  jensenlem2  25725  lgamcvg2  25792  pntrsumo1  26301  clwlknf1oclwwlknlem3  28020  eucrct2eupth  28182  rabfodom  30425  fmptssfisupp  30594  qusima  31166  elrspunidl  31178  poimirlem16  35416  poimirlem19  35419  poimirlem30  35430  ftc1anclem8  35480  ftc2nc  35482  areacirclem2  35489  aks4d1p1p5  39702  evlsval3  39851  evlsbagval  39854  hbtlem6  40526  radcnvrat  41470  disjf1o  42267  cncfmptss  42670  limsupvaluzmpt  42800  supcnvlimsupmpt  42824  dvnprodlem1  43029  iblsplit  43049  itgcoscmulx  43052  itgiccshift  43063  itgperiod  43064  itgsbtaddcnst  43065  dirkercncflem2  43187  dirkercncflem4  43189  fourierdlem28  43218  fourierdlem40  43230  fourierdlem58  43247  fourierdlem74  43263  fourierdlem75  43264  fourierdlem76  43265  fourierdlem78  43267  fourierdlem80  43269  fourierdlem81  43270  fourierdlem84  43273  fourierdlem85  43274  fourierdlem90  43279  fourierdlem93  43282  fourierdlem101  43290  fourierdlem111  43300  sge0lessmpt  43479  sge0gerpmpt  43482  sge0resrnlem  43483  sge0ssrempt  43485  sge0ltfirpmpt  43488  sge0iunmptlemre  43495  sge0lefimpt  43503  sge0ltfirpmpt2  43506  sge0pnffigtmpt  43520  ismeannd  43547  omeiunltfirp  43599  caratheodorylem2  43607  sssmfmpt  43825  gsumsplit2f  44908  funcrngcsetc  45090  funcrngcsetcALT  45091  funcringcsetc  45127  fdmdifeqresdif  45211