Theorem resmptd 6058

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

Syntax hints:   → wi 4   = wceq 1540   ⊆ wss 3951   ↦ cmpt 5225   ↾ cres 5687

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-opab 5206  df-mpt 5226  df-xp 5691  df-rel 5692  df-res 5697

This theorem is referenced by:  f1ossf1o  7148  oacomf1olem  8602  fmptssfisupp  9434  cantnfres  9717  rlimres2  15597  lo1res2  15598  o1res2  15599  fsumss  15761  fprodss  15984  conjsubgen  19269  gsumsplit2  19947  gsum2d  19990  dmdprdsplitlem  20057  dprd2dlem1  20061  funcrngcsetc  20640  funcrngcsetcALT  20641  funcringcsetc  20674  psrlidm  21982  psrridm  21983  mplmonmul  22054  mplcoe1  22055  mplcoe5  22058  evlsval2  22111  mdetunilem9  22626  cmpfi  23416  ptpjopn  23620  xkoptsub  23662  xkopjcn  23664  cnmpt1res  23684  subgntr  24115  opnsubg  24116  clsnsg  24118  snclseqg  24124  tsmsxplem1  24161  imasdsf1olem  24383  subgnm  24646  cphsscph  25285  mbfss  25681  mbflimsup  25701  mbfmullem2  25759  iblss  25840  limcres  25921  dvmptresicc  25951  dvaddbr  25974  dvmulbr  25975  dvmulbrOLD  25976  dvcmulf  25982  dvmptres3  25994  dvmptres2  26000  dvmptntr  26009  lhop2  26054  lhop  26055  dvfsumle  26060  dvfsumleOLD  26061  dvfsumabs  26063  dvfsumlem2  26067  dvfsumlem2OLD  26068  ftc2ditglem  26086  itgsubstlem  26089  itgpowd  26091  mdegfval  26101  psercn2  26466  psercn2OLD  26467  psercn  26470  abelth  26485  abelth2  26486  efrlim  27012  efrlimOLD  27013  jensenlem2  27031  lgamcvg2  27098  pntrsumo1  27609  clwlknf1oclwwlknlem3  30102  eucrct2eupth  30264  rabfodom  32524  qusima  33436  elrspunidl  33456  poimirlem16  37643  poimirlem19  37646  poimirlem30  37657  ftc1anclem8  37707  ftc2nc  37709  areacirclem2  37716  aks4d1p1p5  42076  aks6d1c6lem2  42172  aks6d1c6lem4  42174  evlsval3  42569  selvvvval  42595  evlselv  42597  evlsmhpvvval  42605  hbtlem6  43141  radcnvrat  44333  disjf1o  45196  cncfmptss  45602  limsupvaluzmpt  45732  supcnvlimsupmpt  45756  dvnprodlem1  45961  iblsplit  45981  itgcoscmulx  45984  itgiccshift  45995  itgperiod  45996  itgsbtaddcnst  45997  dirkercncflem2  46119  dirkercncflem4  46121  fourierdlem28  46150  fourierdlem40  46162  fourierdlem58  46179  fourierdlem74  46195  fourierdlem75  46196  fourierdlem76  46197  fourierdlem78  46199  fourierdlem80  46201  fourierdlem81  46202  fourierdlem84  46205  fourierdlem85  46206  fourierdlem90  46211  fourierdlem93  46214  fourierdlem101  46222  fourierdlem111  46232  sge0lessmpt  46414  sge0gerpmpt  46417  sge0resrnlem  46418  sge0ssrempt  46420  sge0ltfirpmpt  46423  sge0iunmptlemre  46430  sge0lefimpt  46438  sge0ltfirpmpt2  46441  sge0pnffigtmpt  46455  ismeannd  46482  omeiunltfirp  46534  caratheodorylem2  46542  sssmfmpt  46765  gsumsplit2f  48096  fdmdifeqresdif  48258