Theorem resmptd 5989

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

Syntax hints:   → wi 4   = wceq 1541   ⊆ wss 3902   ↦ cmpt 5172   ↾ cres 5618

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 2113  ax-9 2121  ax-10 2144  ax-12 2180  ax-ext 2703  ax-sep 5234  ax-nul 5244  ax-pr 5370

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 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4476  df-sn 4577  df-pr 4579  df-op 4583  df-opab 5154  df-mpt 5173  df-xp 5622  df-rel 5623  df-res 5628

This theorem is referenced by:  f1ossf1o  7061  oacomf1olem  8479  fmptssfisupp  9278  cantnfres  9567  rlimres2  15468  lo1res2  15469  o1res2  15470  fsumss  15632  fprodss  15855  conjsubgen  19164  gsumsplit2  19842  gsum2d  19885  dmdprdsplitlem  19952  dprd2dlem1  19956  funcrngcsetc  20556  funcrngcsetcALT  20557  funcringcsetc  20590  psrlidm  21900  psrridm  21901  mplmonmul  21972  mplcoe1  21973  mplcoe5  21976  evlsval2  22023  mdetunilem9  22536  cmpfi  23324  ptpjopn  23528  xkoptsub  23570  xkopjcn  23572  cnmpt1res  23592  subgntr  24023  opnsubg  24024  clsnsg  24026  snclseqg  24032  tsmsxplem1  24069  imasdsf1olem  24289  subgnm  24549  cphsscph  25179  mbfss  25575  mbflimsup  25595  mbfmullem2  25653  iblss  25734  limcres  25815  dvmptresicc  25845  dvaddbr  25868  dvmulbr  25869  dvmulbrOLD  25870  dvcmulf  25876  dvmptres3  25888  dvmptres2  25894  dvmptntr  25903  lhop2  25948  lhop  25949  dvfsumle  25954  dvfsumleOLD  25955  dvfsumabs  25957  dvfsumlem2  25961  dvfsumlem2OLD  25962  ftc2ditglem  25980  itgsubstlem  25983  itgpowd  25985  mdegfval  25995  psercn2  26360  psercn2OLD  26361  psercn  26364  abelth  26379  abelth2  26380  efrlim  26907  efrlimOLD  26908  jensenlem2  26926  lgamcvg2  26993  pntrsumo1  27504  clwlknf1oclwwlknlem3  30061  eucrct2eupth  30223  rabfodom  32483  qusima  33371  elrspunidl  33391  ressply1evls1  33526  poimirlem16  37682  poimirlem19  37685  poimirlem30  37696  ftc1anclem8  37746  ftc2nc  37748  areacirclem2  37755  aks4d1p1p5  42114  aks6d1c6lem2  42210  aks6d1c6lem4  42212  evlsval3  42598  selvvvval  42624  evlselv  42626  evlsmhpvvval  42634  hbtlem6  43168  radcnvrat  44353  disjf1o  45234  cncfmptss  45633  limsupvaluzmpt  45761  supcnvlimsupmpt  45785  dvnprodlem1  45990  iblsplit  46010  itgcoscmulx  46013  itgiccshift  46024  itgperiod  46025  itgsbtaddcnst  46026  dirkercncflem2  46148  dirkercncflem4  46150  fourierdlem28  46179  fourierdlem40  46191  fourierdlem58  46208  fourierdlem74  46224  fourierdlem75  46225  fourierdlem76  46226  fourierdlem78  46228  fourierdlem80  46230  fourierdlem81  46231  fourierdlem84  46234  fourierdlem85  46235  fourierdlem90  46240  fourierdlem93  46243  fourierdlem101  46251  fourierdlem111  46261  sge0lessmpt  46443  sge0gerpmpt  46446  sge0resrnlem  46447  sge0ssrempt  46449  sge0ltfirpmpt  46452  sge0iunmptlemre  46459  sge0lefimpt  46467  sge0ltfirpmpt2  46470  sge0pnffigtmpt  46484  ismeannd  46511  omeiunltfirp  46563  caratheodorylem2  46571  sssmfmpt  46794  gsumsplit2f  48217  fdmdifeqresdif  48379