Theorem resmptd 6040

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

Syntax hints:   → wi 4   = wceq 1541   ⊆ wss 3948   ↦ cmpt 5231   ↾ cres 5678

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pr 5427

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-opab 5211  df-mpt 5232  df-xp 5682  df-rel 5683  df-res 5688

This theorem is referenced by:  f1ossf1o  7128  oacomf1olem  8566  fmptssfisupp  9391  cantnfres  9674  rlimres2  15509  lo1res2  15510  o1res2  15511  fsumss  15675  fprodss  15896  conjsubgen  19165  gsumsplit2  19838  gsum2d  19881  dmdprdsplitlem  19948  dprd2dlem1  19952  psrlidm  21742  psrridm  21743  mplmonmul  21810  mplcoe1  21811  mplcoe5  21814  evlsval2  21869  mdetunilem9  22342  cmpfi  23132  ptpjopn  23336  xkoptsub  23378  xkopjcn  23380  cnmpt1res  23400  subgntr  23831  opnsubg  23832  clsnsg  23834  snclseqg  23840  tsmsxplem1  23877  imasdsf1olem  24099  subgnm  24362  cphsscph  24992  mbfss  25387  mbflimsup  25407  mbfmullem2  25466  iblss  25546  limcres  25627  dvmptresicc  25657  dvaddbr  25679  dvmulbr  25680  dvcmulf  25686  dvmptres3  25697  dvmptres2  25703  dvmptntr  25712  lhop2  25756  lhop  25757  dvfsumle  25762  dvfsumabs  25764  dvfsumlem2  25768  ftc2ditglem  25786  itgsubstlem  25789  itgpowd  25791  mdegfval  25804  psercn2  26159  psercn  26162  abelth  26177  abelth2  26178  efrlim  26698  jensenlem2  26716  lgamcvg2  26783  pntrsumo1  27292  clwlknf1oclwwlknlem3  29591  eucrct2eupth  29753  rabfodom  31998  qusima  32781  elrspunidl  32808  gg-dvmulbr  35461  gg-psercn2  35464  gg-dvfsumle  35468  gg-dvfsumlem2  35469  poimirlem16  36807  poimirlem19  36810  poimirlem30  36821  ftc1anclem8  36871  ftc2nc  36873  areacirclem2  36880  aks4d1p1p5  41246  evlsval3  41433  selvvvval  41459  evlselv  41461  evlsmhpvvval  41469  hbtlem6  42173  radcnvrat  43375  disjf1o  44189  cncfmptss  44602  limsupvaluzmpt  44732  supcnvlimsupmpt  44756  dvnprodlem1  44961  iblsplit  44981  itgcoscmulx  44984  itgiccshift  44995  itgperiod  44996  itgsbtaddcnst  44997  dirkercncflem2  45119  dirkercncflem4  45121  fourierdlem28  45150  fourierdlem40  45162  fourierdlem58  45179  fourierdlem74  45195  fourierdlem75  45196  fourierdlem76  45197  fourierdlem78  45199  fourierdlem80  45201  fourierdlem81  45202  fourierdlem84  45205  fourierdlem85  45206  fourierdlem90  45211  fourierdlem93  45214  fourierdlem101  45222  fourierdlem111  45232  sge0lessmpt  45414  sge0gerpmpt  45417  sge0resrnlem  45418  sge0ssrempt  45420  sge0ltfirpmpt  45423  sge0iunmptlemre  45430  sge0lefimpt  45438  sge0ltfirpmpt2  45441  sge0pnffigtmpt  45455  ismeannd  45482  omeiunltfirp  45534  caratheodorylem2  45542  sssmfmpt  45765  gsumsplit2f  46857  funcrngcsetc  46985  funcrngcsetcALT  46986  funcringcsetc  47022  fdmdifeqresdif  47106