Theorem resmptd 6031

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ⊆ wss 3895   ↦ cmpt 5185   ↾ cres 5652

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-opab 5167  df-mpt 5186  df-xp 5656  df-rel 5657  df-res 5662

This theorem is used by:  f1ossf1o  7129  oacomf1olem  8575  fmptssfisupp  9389  cantnfres  9681  rlimres2  15733  lo1res2  15734  o1res2  15735  fsumss  15896  fprodss  16120  conjsubgen  19470  gsumsplit2  20148  gsum2d  20191  dmdprdsplitlem  20258  dprd2dlem1  20262  funcrngcsetc  20897  funcrngcsetcALT  20898  funcringcsetc  20931  psrlidm  22274  psrridm  22275  mplmonmul  22350  mplcoe1  22351  mplcoe5  22354  evlsval2  22401  evlsval3  22403  selvvvval  22456  mdetunilem9  22940  cmpfi  23731  ptpjopn  23936  xkoptsub  23978  xkopjcn  23980  cnmpt1res  24000  subgntr  24431  opnsubg  24432  clsnsg  24434  snclseqg  24440  tsmsxplem1  24477  imasdsf1olem  24697  subgnm  24957  cphsscph  25577  mbfss  25972  mbflimsup  25992  mbfmullem2  26050  iblss  26130  limcres  26211  dvmptresicc  26241  dvaddbr  26263  dvmulbr  26264  dvcmulf  26270  dvmptres3  26281  dvmptres2  26287  dvmptntr  26296  lhop2  26340  lhop  26341  dvfsumle  26346  dvfsumabs  26348  dvfsumlem2  26352  ftc2ditglem  26370  itgsubstlem  26373  itgpowd  26375  mdegfval  26385  psercn2  26755  psercn  26758  abelth  26773  abelth2  26774  efrlim  27302  jensenlem2  27320  lgamcvg2  27387  pntrsumo1  27897  clwlknf1oclwwlknlem3  30679  eucrct2eupth  30851  rabfodom  33148  gsummptfsres  33661  qusima  34005  elrspunidl  34024  ressply1evls1  34143  psrmonmul  34228  poimirlem16  38647  poimirlem19  38650  poimirlem30  38661  ftc1anclem8  38711  ftc2nc  38713  areacirclem2  38720  aks4d1p1p5  43218  aks6d1c6lem2  43314  aks6d1c6lem4  43316  evlselv  43710  evlsmhpvvval  43716  hbtlem6  44224  radcnvrat  45391  disjf1o  46299  cncfmptss  46692  limsupvaluzmpt  46820  supcnvlimsupmpt  46844  dvnprodlem1  47049  iblsplit  47069  itgcoscmulx  47072  itgiccshift  47083  itgperiod  47084  itgsbtaddcnst  47085  dirkercncflem2  47207  dirkercncflem4  47209  fourierdlem28  47238  fourierdlem40  47250  fourierdlem58  47267  fourierdlem74  47283  fourierdlem75  47284  fourierdlem76  47285  fourierdlem78  47287  fourierdlem80  47289  fourierdlem81  47290  fourierdlem84  47293  fourierdlem85  47294  fourierdlem90  47299  fourierdlem93  47302  fourierdlem101  47310  fourierdlem111  47320  sge0lessmpt  47502  sge0gerpmpt  47505  sge0resrnlem  47506  sge0ssrempt  47508  sge0ltfirpmpt  47511  sge0iunmptlemre  47518  sge0lefimpt  47526  sge0ltfirpmpt2  47529  sge0pnffigtmpt  47543  ismeannd  47570  omeiunltfirp  47622  caratheodorylem2  47630  sssmfmpt  47853  gsumsplit2f  49370  fdmdifeqresdif  49547