Theorem resmptd 5948

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

Syntax hints:   → wi 4   = wceq 1539   ⊆ wss 3887   ↦ cmpt 5157   ↾ cres 5591

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-opab 5137  df-mpt 5158  df-xp 5595  df-rel 5596  df-res 5601

This theorem is referenced by:  f1ossf1o  7000  oacomf1olem  8395  cantnfres  9435  rlimres2  15270  lo1res2  15271  o1res2  15272  fsumss  15437  fprodss  15658  conjsubgen  18867  gsumsplit2  19530  gsum2d  19573  dmdprdsplitlem  19640  dprd2dlem1  19644  psrlidm  21172  psrridm  21173  mplmonmul  21237  mplcoe1  21238  mplcoe5  21241  evlsval2  21297  mdetunilem9  21769  cmpfi  22559  ptpjopn  22763  xkoptsub  22805  xkopjcn  22807  cnmpt1res  22827  subgntr  23258  opnsubg  23259  clsnsg  23261  snclseqg  23267  tsmsxplem1  23304  imasdsf1olem  23526  subgnm  23789  cphsscph  24415  mbfss  24810  mbflimsup  24830  mbfmullem2  24889  iblss  24969  limcres  25050  dvmptresicc  25080  dvaddbr  25102  dvmulbr  25103  dvcmulf  25109  dvmptres3  25120  dvmptres2  25126  dvmptntr  25135  lhop2  25179  lhop  25180  dvfsumle  25185  dvfsumabs  25187  dvfsumlem2  25191  ftc2ditglem  25209  itgsubstlem  25212  itgpowd  25214  mdegfval  25227  psercn2  25582  psercn  25585  abelth  25600  abelth2  25601  efrlim  26119  jensenlem2  26137  lgamcvg2  26204  pntrsumo1  26713  clwlknf1oclwwlknlem3  28447  eucrct2eupth  28609  rabfodom  30851  fmptssfisupp  31019  qusima  31594  elrspunidl  31606  poimirlem16  35793  poimirlem19  35796  poimirlem30  35807  ftc1anclem8  35857  ftc2nc  35859  areacirclem2  35866  aks4d1p1p5  40083  evlsval3  40272  evlsbagval  40275  hbtlem6  40954  radcnvrat  41932  disjf1o  42729  cncfmptss  43128  limsupvaluzmpt  43258  supcnvlimsupmpt  43282  dvnprodlem1  43487  iblsplit  43507  itgcoscmulx  43510  itgiccshift  43521  itgperiod  43522  itgsbtaddcnst  43523  dirkercncflem2  43645  dirkercncflem4  43647  fourierdlem28  43676  fourierdlem40  43688  fourierdlem58  43705  fourierdlem74  43721  fourierdlem75  43722  fourierdlem76  43723  fourierdlem78  43725  fourierdlem80  43727  fourierdlem81  43728  fourierdlem84  43731  fourierdlem85  43732  fourierdlem90  43737  fourierdlem93  43740  fourierdlem101  43748  fourierdlem111  43758  sge0lessmpt  43937  sge0gerpmpt  43940  sge0resrnlem  43941  sge0ssrempt  43943  sge0ltfirpmpt  43946  sge0iunmptlemre  43953  sge0lefimpt  43961  sge0ltfirpmpt2  43964  sge0pnffigtmpt  43978  ismeannd  44005  omeiunltfirp  44057  caratheodorylem2  44065  sssmfmpt  44286  gsumsplit2f  45374  funcrngcsetc  45556  funcrngcsetcALT  45557  funcringcsetc  45593  fdmdifeqresdif  45677