Theorem resmptd 6033

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

Syntax hints:   → wi 4   = wceq 1563   ⊆ wss 3907   ↦ cmpt 5186   ↾ cres 5654

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-12 2215  ax-ext 2737  ax-sep 5251  ax-pr 5395

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-opab 5168  df-mpt 5187  df-xp 5658  df-rel 5659  df-res 5664

This theorem is referenced by:  f1ossf1o  7114  oacomf1olem  8537  fmptssfisupp  9342  cantnfres  9634  rlimres2  15602  lo1res2  15603  o1res2  15604  fsumss  15766  fprodss  15992  conjsubgen  19312  gsumsplit2  19990  gsum2d  20033  dmdprdsplitlem  20100  dprd2dlem1  20104  funcrngcsetc  20716  funcrngcsetcALT  20717  funcringcsetc  20750  psrlidm  22071  psrridm  22072  mplmonmul  22147  mplcoe1  22148  mplcoe5  22151  evlsval2  22198  evlsval3  22200  selvvvval  22253  mdetunilem9  22738  cmpfi  23526  ptpjopn  23730  xkoptsub  23772  xkopjcn  23774  cnmpt1res  23794  subgntr  24225  opnsubg  24226  clsnsg  24228  snclseqg  24234  tsmsxplem1  24271  imasdsf1olem  24491  subgnm  24751  cphsscph  25371  mbfss  25766  mbflimsup  25786  mbfmullem2  25844  iblss  25925  limcres  26006  dvmptresicc  26036  dvaddbr  26058  dvmulbr  26059  dvcmulf  26065  dvmptres3  26076  dvmptres2  26082  dvmptntr  26091  lhop2  26135  lhop  26136  dvfsumle  26141  dvfsumabs  26143  dvfsumlem2  26147  ftc2ditglem  26165  itgsubstlem  26168  itgpowd  26170  mdegfval  26180  psercn2  26544  psercn  26547  abelth  26562  abelth2  26563  efrlim  27092  jensenlem2  27110  lgamcvg2  27177  pntrsumo1  27687  clwlknf1oclwwlknlem3  30343  eucrct2eupth  30505  rabfodom  32761  gsummptfsres  33287  qusima  33633  elrspunidl  33652  ressply1evls1  33772  psrmonmul  33857  poimirlem16  38147  poimirlem19  38150  poimirlem30  38161  ftc1anclem8  38211  ftc2nc  38213  areacirclem2  38220  aks4d1p1p5  42704  aks6d1c6lem2  42800  aks6d1c6lem4  42802  evlselv  43183  evlsmhpvvval  43189  hbtlem6  43718  radcnvrat  44888  disjf1o  45767  cncfmptss  46161  limsupvaluzmpt  46289  supcnvlimsupmpt  46313  dvnprodlem1  46518  iblsplit  46538  itgcoscmulx  46541  itgiccshift  46552  itgperiod  46553  itgsbtaddcnst  46554  dirkercncflem2  46676  dirkercncflem4  46678  fourierdlem28  46707  fourierdlem40  46719  fourierdlem58  46736  fourierdlem74  46752  fourierdlem75  46753  fourierdlem76  46754  fourierdlem78  46756  fourierdlem80  46758  fourierdlem81  46759  fourierdlem84  46762  fourierdlem85  46763  fourierdlem90  46768  fourierdlem93  46771  fourierdlem101  46779  fourierdlem111  46789  sge0lessmpt  46971  sge0gerpmpt  46974  sge0resrnlem  46975  sge0ssrempt  46977  sge0ltfirpmpt  46980  sge0iunmptlemre  46987  sge0lefimpt  46995  sge0ltfirpmpt2  46998  sge0pnffigtmpt  47012  ismeannd  47039  omeiunltfirp  47091  caratheodorylem2  47099  sssmfmpt  47322  gsumsplit2f  48800  fdmdifeqresdif  48973