Theorem resmptd 6011

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

Syntax hints:   → wi 4   = wceq 1540   ⊆ wss 3914   ↦ cmpt 5188   ↾ cres 5640

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-opab 5170  df-mpt 5189  df-xp 5644  df-rel 5645  df-res 5650

This theorem is referenced by:  f1ossf1o  7100  oacomf1olem  8528  fmptssfisupp  9345  cantnfres  9630  rlimres2  15527  lo1res2  15528  o1res2  15529  fsumss  15691  fprodss  15914  conjsubgen  19183  gsumsplit2  19859  gsum2d  19902  dmdprdsplitlem  19969  dprd2dlem1  19973  funcrngcsetc  20549  funcrngcsetcALT  20550  funcringcsetc  20583  psrlidm  21871  psrridm  21872  mplmonmul  21943  mplcoe1  21944  mplcoe5  21947  evlsval2  21994  mdetunilem9  22507  cmpfi  23295  ptpjopn  23499  xkoptsub  23541  xkopjcn  23543  cnmpt1res  23563  subgntr  23994  opnsubg  23995  clsnsg  23997  snclseqg  24003  tsmsxplem1  24040  imasdsf1olem  24261  subgnm  24521  cphsscph  25151  mbfss  25547  mbflimsup  25567  mbfmullem2  25625  iblss  25706  limcres  25787  dvmptresicc  25817  dvaddbr  25840  dvmulbr  25841  dvmulbrOLD  25842  dvcmulf  25848  dvmptres3  25860  dvmptres2  25866  dvmptntr  25875  lhop2  25920  lhop  25921  dvfsumle  25926  dvfsumleOLD  25927  dvfsumabs  25929  dvfsumlem2  25933  dvfsumlem2OLD  25934  ftc2ditglem  25952  itgsubstlem  25955  itgpowd  25957  mdegfval  25967  psercn2  26332  psercn2OLD  26333  psercn  26336  abelth  26351  abelth2  26352  efrlim  26879  efrlimOLD  26880  jensenlem2  26898  lgamcvg2  26965  pntrsumo1  27476  clwlknf1oclwwlknlem3  30012  eucrct2eupth  30174  rabfodom  32434  qusima  33379  elrspunidl  33399  ressply1evls1  33534  poimirlem16  37630  poimirlem19  37633  poimirlem30  37644  ftc1anclem8  37694  ftc2nc  37696  areacirclem2  37703  aks4d1p1p5  42063  aks6d1c6lem2  42159  aks6d1c6lem4  42161  evlsval3  42547  selvvvval  42573  evlselv  42575  evlsmhpvvval  42583  hbtlem6  43118  radcnvrat  44303  disjf1o  45185  cncfmptss  45585  limsupvaluzmpt  45715  supcnvlimsupmpt  45739  dvnprodlem1  45944  iblsplit  45964  itgcoscmulx  45967  itgiccshift  45978  itgperiod  45979  itgsbtaddcnst  45980  dirkercncflem2  46102  dirkercncflem4  46104  fourierdlem28  46133  fourierdlem40  46145  fourierdlem58  46162  fourierdlem74  46178  fourierdlem75  46179  fourierdlem76  46180  fourierdlem78  46182  fourierdlem80  46184  fourierdlem81  46185  fourierdlem84  46188  fourierdlem85  46189  fourierdlem90  46194  fourierdlem93  46197  fourierdlem101  46205  fourierdlem111  46215  sge0lessmpt  46397  sge0gerpmpt  46400  sge0resrnlem  46401  sge0ssrempt  46403  sge0ltfirpmpt  46406  sge0iunmptlemre  46413  sge0lefimpt  46421  sge0ltfirpmpt2  46424  sge0pnffigtmpt  46438  ismeannd  46465  omeiunltfirp  46517  caratheodorylem2  46525  sssmfmpt  46748  gsumsplit2f  48168  fdmdifeqresdif  48330