Theorem resmptd 6060

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

Syntax hints:   → wi 4   = wceq 1537   ⊆ wss 3963   ↦ cmpt 5231   ↾ cres 5691

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-opab 5211  df-mpt 5232  df-xp 5695  df-rel 5696  df-res 5701

This theorem is referenced by:  f1ossf1o  7148  oacomf1olem  8601  fmptssfisupp  9432  cantnfres  9715  rlimres2  15594  lo1res2  15595  o1res2  15596  fsumss  15758  fprodss  15981  conjsubgen  19282  gsumsplit2  19962  gsum2d  20005  dmdprdsplitlem  20072  dprd2dlem1  20076  funcrngcsetc  20657  funcrngcsetcALT  20658  funcringcsetc  20691  psrlidm  22000  psrridm  22001  mplmonmul  22072  mplcoe1  22073  mplcoe5  22076  evlsval2  22129  mdetunilem9  22642  cmpfi  23432  ptpjopn  23636  xkoptsub  23678  xkopjcn  23680  cnmpt1res  23700  subgntr  24131  opnsubg  24132  clsnsg  24134  snclseqg  24140  tsmsxplem1  24177  imasdsf1olem  24399  subgnm  24662  cphsscph  25299  mbfss  25695  mbflimsup  25715  mbfmullem2  25774  iblss  25855  limcres  25936  dvmptresicc  25966  dvaddbr  25989  dvmulbr  25990  dvmulbrOLD  25991  dvcmulf  25997  dvmptres3  26009  dvmptres2  26015  dvmptntr  26024  lhop2  26069  lhop  26070  dvfsumle  26075  dvfsumleOLD  26076  dvfsumabs  26078  dvfsumlem2  26082  dvfsumlem2OLD  26083  ftc2ditglem  26101  itgsubstlem  26104  itgpowd  26106  mdegfval  26116  psercn2  26481  psercn2OLD  26482  psercn  26485  abelth  26500  abelth2  26501  efrlim  27027  efrlimOLD  27028  jensenlem2  27046  lgamcvg2  27113  pntrsumo1  27624  clwlknf1oclwwlknlem3  30112  eucrct2eupth  30274  rabfodom  32533  qusima  33416  elrspunidl  33436  poimirlem16  37623  poimirlem19  37626  poimirlem30  37637  ftc1anclem8  37687  ftc2nc  37689  areacirclem2  37696  aks4d1p1p5  42057  aks6d1c6lem2  42153  aks6d1c6lem4  42155  evlsval3  42546  selvvvval  42572  evlselv  42574  evlsmhpvvval  42582  hbtlem6  43118  radcnvrat  44310  disjf1o  45134  cncfmptss  45543  limsupvaluzmpt  45673  supcnvlimsupmpt  45697  dvnprodlem1  45902  iblsplit  45922  itgcoscmulx  45925  itgiccshift  45936  itgperiod  45937  itgsbtaddcnst  45938  dirkercncflem2  46060  dirkercncflem4  46062  fourierdlem28  46091  fourierdlem40  46103  fourierdlem58  46120  fourierdlem74  46136  fourierdlem75  46137  fourierdlem76  46138  fourierdlem78  46140  fourierdlem80  46142  fourierdlem81  46143  fourierdlem84  46146  fourierdlem85  46147  fourierdlem90  46152  fourierdlem93  46155  fourierdlem101  46163  fourierdlem111  46173  sge0lessmpt  46355  sge0gerpmpt  46358  sge0resrnlem  46359  sge0ssrempt  46361  sge0ltfirpmpt  46364  sge0iunmptlemre  46371  sge0lefimpt  46379  sge0ltfirpmpt2  46382  sge0pnffigtmpt  46396  ismeannd  46423  omeiunltfirp  46475  caratheodorylem2  46483  sssmfmpt  46706  gsumsplit2f  48024  fdmdifeqresdif  48187