Theorem resmptd 5999

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

Syntax hints:   → wi 4   = wceq 1541   ⊆ wss 3901   ↦ cmpt 5179   ↾ cres 5626

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-opab 5161  df-mpt 5180  df-xp 5630  df-rel 5631  df-res 5636

This theorem is referenced by:  f1ossf1o  7073  oacomf1olem  8491  fmptssfisupp  9297  cantnfres  9586  rlimres2  15484  lo1res2  15485  o1res2  15486  fsumss  15648  fprodss  15871  conjsubgen  19180  gsumsplit2  19858  gsum2d  19901  dmdprdsplitlem  19968  dprd2dlem1  19972  funcrngcsetc  20573  funcrngcsetcALT  20574  funcringcsetc  20607  psrlidm  21917  psrridm  21918  mplmonmul  21991  mplcoe1  21992  mplcoe5  21995  evlsval2  22042  evlsval3  22044  mdetunilem9  22564  cmpfi  23352  ptpjopn  23556  xkoptsub  23598  xkopjcn  23600  cnmpt1res  23620  subgntr  24051  opnsubg  24052  clsnsg  24054  snclseqg  24060  tsmsxplem1  24097  imasdsf1olem  24317  subgnm  24577  cphsscph  25207  mbfss  25603  mbflimsup  25623  mbfmullem2  25681  iblss  25762  limcres  25843  dvmptresicc  25873  dvaddbr  25896  dvmulbr  25897  dvmulbrOLD  25898  dvcmulf  25904  dvmptres3  25916  dvmptres2  25922  dvmptntr  25931  lhop2  25976  lhop  25977  dvfsumle  25982  dvfsumleOLD  25983  dvfsumabs  25985  dvfsumlem2  25989  dvfsumlem2OLD  25990  ftc2ditglem  26008  itgsubstlem  26011  itgpowd  26013  mdegfval  26023  psercn2  26388  psercn2OLD  26389  psercn  26392  abelth  26407  abelth2  26408  efrlim  26935  efrlimOLD  26936  jensenlem2  26954  lgamcvg2  27021  pntrsumo1  27532  clwlknf1oclwwlknlem3  30158  eucrct2eupth  30320  rabfodom  32580  gsummptfsres  33137  qusima  33489  elrspunidl  33509  ressply1evls1  33646  poimirlem16  37833  poimirlem19  37836  poimirlem30  37847  ftc1anclem8  37897  ftc2nc  37899  areacirclem2  37906  aks4d1p1p5  42325  aks6d1c6lem2  42421  aks6d1c6lem4  42423  selvvvval  42824  evlselv  42826  evlsmhpvvval  42834  hbtlem6  43367  radcnvrat  44551  disjf1o  45431  cncfmptss  45829  limsupvaluzmpt  45957  supcnvlimsupmpt  45981  dvnprodlem1  46186  iblsplit  46206  itgcoscmulx  46209  itgiccshift  46220  itgperiod  46221  itgsbtaddcnst  46222  dirkercncflem2  46344  dirkercncflem4  46346  fourierdlem28  46375  fourierdlem40  46387  fourierdlem58  46404  fourierdlem74  46420  fourierdlem75  46421  fourierdlem76  46422  fourierdlem78  46424  fourierdlem80  46426  fourierdlem81  46427  fourierdlem84  46430  fourierdlem85  46431  fourierdlem90  46436  fourierdlem93  46439  fourierdlem101  46447  fourierdlem111  46457  sge0lessmpt  46639  sge0gerpmpt  46642  sge0resrnlem  46643  sge0ssrempt  46645  sge0ltfirpmpt  46648  sge0iunmptlemre  46655  sge0lefimpt  46663  sge0ltfirpmpt2  46666  sge0pnffigtmpt  46680  ismeannd  46707  omeiunltfirp  46759  caratheodorylem2  46767  sssmfmpt  46990  gsumsplit2f  48422  fdmdifeqresdif  48584