Theorem resmptd 6026

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

Syntax hints:   → wi 4   = wceq 1559   ⊆ wss 3904   ↦ cmpt 5180   ↾ cres 5647

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-12 2211  ax-ext 2733  ax-sep 5245  ax-pr 5389

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3455  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4480  df-sn 4582  df-pr 4584  df-op 4588  df-opab 5162  df-mpt 5181  df-xp 5651  df-rel 5652  df-res 5657

This theorem is referenced by:  f1ossf1o  7106  oacomf1olem  8528  fmptssfisupp  9337  cantnfres  9629  rlimres2  15571  lo1res2  15572  o1res2  15573  fsumss  15735  fprodss  15961  conjsubgen  19274  gsumsplit2  19952  gsum2d  19995  dmdprdsplitlem  20062  dprd2dlem1  20066  funcrngcsetc  20669  funcrngcsetcALT  20670  funcringcsetc  20703  psrlidm  21993  psrridm  21994  mplmonmul  22069  mplcoe1  22070  mplcoe5  22073  evlsval2  22120  evlsval3  22122  selvvvval  22175  mdetunilem9  22660  cmpfi  23448  ptpjopn  23652  xkoptsub  23694  xkopjcn  23696  cnmpt1res  23716  subgntr  24147  opnsubg  24148  clsnsg  24150  snclseqg  24156  tsmsxplem1  24193  imasdsf1olem  24413  subgnm  24673  cphsscph  25293  mbfss  25688  mbflimsup  25708  mbfmullem2  25766  iblss  25847  limcres  25928  dvmptresicc  25958  dvaddbr  25980  dvmulbr  25981  dvcmulf  25987  dvmptres3  25998  dvmptres2  26004  dvmptntr  26013  lhop2  26057  lhop  26058  dvfsumle  26063  dvfsumabs  26065  dvfsumlem2  26069  ftc2ditglem  26087  itgsubstlem  26090  itgpowd  26092  mdegfval  26102  psercn2  26463  psercn  26466  abelth  26481  abelth2  26482  efrlim  27011  jensenlem2  27029  lgamcvg2  27096  pntrsumo1  27606  clwlknf1oclwwlknlem3  30231  eucrct2eupth  30393  rabfodom  32653  gsummptfsres  33195  qusima  33555  elrspunidl  33575  ressply1evls1  33722  psrmonmul  33808  poimirlem16  38099  poimirlem19  38102  poimirlem30  38113  ftc1anclem8  38163  ftc2nc  38165  areacirclem2  38172  aks4d1p1p5  42656  aks6d1c6lem2  42752  aks6d1c6lem4  42754  evlselv  43135  evlsmhpvvval  43141  hbtlem6  43670  radcnvrat  44854  disjf1o  45733  cncfmptss  46127  limsupvaluzmpt  46255  supcnvlimsupmpt  46279  dvnprodlem1  46484  iblsplit  46504  itgcoscmulx  46507  itgiccshift  46518  itgperiod  46519  itgsbtaddcnst  46520  dirkercncflem2  46642  dirkercncflem4  46644  fourierdlem28  46673  fourierdlem40  46685  fourierdlem58  46702  fourierdlem74  46718  fourierdlem75  46719  fourierdlem76  46720  fourierdlem78  46722  fourierdlem80  46724  fourierdlem81  46725  fourierdlem84  46728  fourierdlem85  46729  fourierdlem90  46734  fourierdlem93  46737  fourierdlem101  46745  fourierdlem111  46755  sge0lessmpt  46937  sge0gerpmpt  46940  sge0resrnlem  46941  sge0ssrempt  46943  sge0ltfirpmpt  46946  sge0iunmptlemre  46953  sge0lefimpt  46961  sge0ltfirpmpt2  46964  sge0pnffigtmpt  46978  ismeannd  47005  omeiunltfirp  47057  caratheodorylem2  47065  sssmfmpt  47288  gsumsplit2f  48766  fdmdifeqresdif  48928