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 1540   ⊆ 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 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-12 2170  ax-ext 2702  ax-sep 5299  ax-nul 5306  ax-pr 5427

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3432  df-v 3475  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  8570  fmptssfisupp  9395  cantnfres  9678  rlimres2  15512  lo1res2  15513  o1res2  15514  fsumss  15678  fprodss  15899  conjsubgen  19172  gsumsplit2  19845  gsum2d  19888  dmdprdsplitlem  19955  dprd2dlem1  19959  funcrngcsetc  20532  funcrngcsetcALT  20533  funcringcsetc  20566  psrlidm  21834  psrridm  21835  mplmonmul  21902  mplcoe1  21903  mplcoe5  21906  evlsval2  21961  mdetunilem9  22442  cmpfi  23232  ptpjopn  23436  xkoptsub  23478  xkopjcn  23480  cnmpt1res  23500  subgntr  23931  opnsubg  23932  clsnsg  23934  snclseqg  23940  tsmsxplem1  23977  imasdsf1olem  24199  subgnm  24462  cphsscph  25099  mbfss  25495  mbflimsup  25515  mbfmullem2  25574  iblss  25654  limcres  25735  dvmptresicc  25765  dvaddbr  25788  dvmulbr  25789  dvmulbrOLD  25790  dvcmulf  25796  dvmptres3  25808  dvmptres2  25814  dvmptntr  25823  lhop2  25868  lhop  25869  dvfsumle  25874  dvfsumleOLD  25875  dvfsumabs  25877  dvfsumlem2  25881  dvfsumlem2OLD  25882  ftc2ditglem  25900  itgsubstlem  25903  itgpowd  25905  mdegfval  25918  psercn2  26274  psercn2OLD  26275  psercn  26278  abelth  26293  abelth2  26294  efrlim  26815  jensenlem2  26833  lgamcvg2  26900  pntrsumo1  27411  clwlknf1oclwwlknlem3  29769  eucrct2eupth  29931  rabfodom  32176  qusima  32959  elrspunidl  32986  poimirlem16  36968  poimirlem19  36971  poimirlem30  36982  ftc1anclem8  37032  ftc2nc  37034  areacirclem2  37041  aks4d1p1p5  41407  evlsval3  41594  selvvvval  41620  evlselv  41622  evlsmhpvvval  41630  hbtlem6  42334  radcnvrat  43536  disjf1o  44349  cncfmptss  44762  limsupvaluzmpt  44892  supcnvlimsupmpt  44916  dvnprodlem1  45121  iblsplit  45141  itgcoscmulx  45144  itgiccshift  45155  itgperiod  45156  itgsbtaddcnst  45157  dirkercncflem2  45279  dirkercncflem4  45281  fourierdlem28  45310  fourierdlem40  45322  fourierdlem58  45339  fourierdlem74  45355  fourierdlem75  45356  fourierdlem76  45357  fourierdlem78  45359  fourierdlem80  45361  fourierdlem81  45362  fourierdlem84  45365  fourierdlem85  45366  fourierdlem90  45371  fourierdlem93  45374  fourierdlem101  45382  fourierdlem111  45392  sge0lessmpt  45574  sge0gerpmpt  45577  sge0resrnlem  45578  sge0ssrempt  45580  sge0ltfirpmpt  45583  sge0iunmptlemre  45590  sge0lefimpt  45598  sge0ltfirpmpt2  45601  sge0pnffigtmpt  45615  ismeannd  45642  omeiunltfirp  45694  caratheodorylem2  45702  sssmfmpt  45925  gsumsplit2f  47017  fdmdifeqresdif  47180