Theorem resmptd 6005

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

Syntax hints:   → wi 4   = wceq 1542   ⊆ wss 3889   ↦ cmpt 5166   ↾ cres 5633

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 2708  ax-sep 5231  ax-pr 5375

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 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-opab 5148  df-mpt 5167  df-xp 5637  df-rel 5638  df-res 5643

This theorem is referenced by:  f1ossf1o  7081  oacomf1olem  8499  fmptssfisupp  9307  cantnfres  9598  rlimres2  15523  lo1res2  15524  o1res2  15525  fsumss  15687  fprodss  15913  conjsubgen  19226  gsumsplit2  19904  gsum2d  19947  dmdprdsplitlem  20014  dprd2dlem1  20018  funcrngcsetc  20617  funcrngcsetcALT  20618  funcringcsetc  20651  psrlidm  21940  psrridm  21941  mplmonmul  22014  mplcoe1  22015  mplcoe5  22018  evlsval2  22065  evlsval3  22067  mdetunilem9  22585  cmpfi  23373  ptpjopn  23577  xkoptsub  23619  xkopjcn  23621  cnmpt1res  23641  subgntr  24072  opnsubg  24073  clsnsg  24075  snclseqg  24081  tsmsxplem1  24118  imasdsf1olem  24338  subgnm  24598  cphsscph  25218  mbfss  25613  mbflimsup  25633  mbfmullem2  25691  iblss  25772  limcres  25853  dvmptresicc  25883  dvaddbr  25905  dvmulbr  25906  dvcmulf  25912  dvmptres3  25923  dvmptres2  25929  dvmptntr  25938  lhop2  25982  lhop  25983  dvfsumle  25988  dvfsumabs  25990  dvfsumlem2  25994  ftc2ditglem  26012  itgsubstlem  26015  itgpowd  26017  mdegfval  26027  psercn2  26388  psercn  26391  abelth  26406  abelth2  26407  efrlim  26933  jensenlem2  26951  lgamcvg2  27018  pntrsumo1  27528  clwlknf1oclwwlknlem3  30153  eucrct2eupth  30315  rabfodom  32575  gsummptfsres  33115  qusima  33468  elrspunidl  33488  ressply1evls1  33625  psrmonmul  33694  poimirlem16  37957  poimirlem19  37960  poimirlem30  37971  ftc1anclem8  38021  ftc2nc  38023  areacirclem2  38030  aks4d1p1p5  42514  aks6d1c6lem2  42610  aks6d1c6lem4  42612  selvvvval  43018  evlselv  43020  evlsmhpvvval  43028  hbtlem6  43557  radcnvrat  44741  disjf1o  45621  cncfmptss  46017  limsupvaluzmpt  46145  supcnvlimsupmpt  46169  dvnprodlem1  46374  iblsplit  46394  itgcoscmulx  46397  itgiccshift  46408  itgperiod  46409  itgsbtaddcnst  46410  dirkercncflem2  46532  dirkercncflem4  46534  fourierdlem28  46563  fourierdlem40  46575  fourierdlem58  46592  fourierdlem74  46608  fourierdlem75  46609  fourierdlem76  46610  fourierdlem78  46612  fourierdlem80  46614  fourierdlem81  46615  fourierdlem84  46618  fourierdlem85  46619  fourierdlem90  46624  fourierdlem93  46627  fourierdlem101  46635  fourierdlem111  46645  sge0lessmpt  46827  sge0gerpmpt  46830  sge0resrnlem  46831  sge0ssrempt  46833  sge0ltfirpmpt  46836  sge0iunmptlemre  46843  sge0lefimpt  46851  sge0ltfirpmpt2  46854  sge0pnffigtmpt  46868  ismeannd  46895  omeiunltfirp  46947  caratheodorylem2  46955  sssmfmpt  47178  gsumsplit2f  48656  fdmdifeqresdif  48818