Theorem resmptd 6007

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

Syntax hints:   → wi 4   = wceq 1542   ⊆ wss 3903   ↦ cmpt 5181   ↾ cres 5634

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-opab 5163  df-mpt 5182  df-xp 5638  df-rel 5639  df-res 5644

This theorem is referenced by:  f1ossf1o  7083  oacomf1olem  8501  fmptssfisupp  9309  cantnfres  9598  rlimres2  15496  lo1res2  15497  o1res2  15498  fsumss  15660  fprodss  15883  conjsubgen  19192  gsumsplit2  19870  gsum2d  19913  dmdprdsplitlem  19980  dprd2dlem1  19984  funcrngcsetc  20585  funcrngcsetcALT  20586  funcringcsetc  20619  psrlidm  21929  psrridm  21930  mplmonmul  22003  mplcoe1  22004  mplcoe5  22007  evlsval2  22054  evlsval3  22056  mdetunilem9  22576  cmpfi  23364  ptpjopn  23568  xkoptsub  23610  xkopjcn  23612  cnmpt1res  23632  subgntr  24063  opnsubg  24064  clsnsg  24066  snclseqg  24072  tsmsxplem1  24109  imasdsf1olem  24329  subgnm  24589  cphsscph  25219  mbfss  25615  mbflimsup  25635  mbfmullem2  25693  iblss  25774  limcres  25855  dvmptresicc  25885  dvaddbr  25908  dvmulbr  25909  dvmulbrOLD  25910  dvcmulf  25916  dvmptres3  25928  dvmptres2  25934  dvmptntr  25943  lhop2  25988  lhop  25989  dvfsumle  25994  dvfsumleOLD  25995  dvfsumabs  25997  dvfsumlem2  26001  dvfsumlem2OLD  26002  ftc2ditglem  26020  itgsubstlem  26023  itgpowd  26025  mdegfval  26035  psercn2  26400  psercn2OLD  26401  psercn  26404  abelth  26419  abelth2  26420  efrlim  26947  efrlimOLD  26948  jensenlem2  26966  lgamcvg2  27033  pntrsumo1  27544  clwlknf1oclwwlknlem3  30170  eucrct2eupth  30332  rabfodom  32591  gsummptfsres  33147  qusima  33500  elrspunidl  33520  ressply1evls1  33657  psrmonmul  33726  poimirlem16  37881  poimirlem19  37884  poimirlem30  37895  ftc1anclem8  37945  ftc2nc  37947  areacirclem2  37954  aks4d1p1p5  42439  aks6d1c6lem2  42535  aks6d1c6lem4  42537  selvvvval  42937  evlselv  42939  evlsmhpvvval  42947  hbtlem6  43480  radcnvrat  44664  disjf1o  45544  cncfmptss  45941  limsupvaluzmpt  46069  supcnvlimsupmpt  46093  dvnprodlem1  46298  iblsplit  46318  itgcoscmulx  46321  itgiccshift  46332  itgperiod  46333  itgsbtaddcnst  46334  dirkercncflem2  46456  dirkercncflem4  46458  fourierdlem28  46487  fourierdlem40  46499  fourierdlem58  46516  fourierdlem74  46532  fourierdlem75  46533  fourierdlem76  46534  fourierdlem78  46536  fourierdlem80  46538  fourierdlem81  46539  fourierdlem84  46542  fourierdlem85  46543  fourierdlem90  46548  fourierdlem93  46551  fourierdlem101  46559  fourierdlem111  46569  sge0lessmpt  46751  sge0gerpmpt  46754  sge0resrnlem  46755  sge0ssrempt  46757  sge0ltfirpmpt  46760  sge0iunmptlemre  46767  sge0lefimpt  46775  sge0ltfirpmpt2  46778  sge0pnffigtmpt  46792  ismeannd  46819  omeiunltfirp  46871  caratheodorylem2  46879  sssmfmpt  47102  gsumsplit2f  48534  fdmdifeqresdif  48696