Theorem resmptd 5988

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

Syntax hints:   → wi 4   = wceq 1541   ⊆ wss 3897   ↦ cmpt 5170   ↾ cres 5616

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 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-12 2180  ax-ext 2703  ax-sep 5232  ax-nul 5242  ax-pr 5368

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-opab 5152  df-mpt 5171  df-xp 5620  df-rel 5621  df-res 5626

This theorem is referenced by:  f1ossf1o  7061  oacomf1olem  8479  fmptssfisupp  9278  cantnfres  9567  rlimres2  15468  lo1res2  15469  o1res2  15470  fsumss  15632  fprodss  15855  conjsubgen  19163  gsumsplit2  19841  gsum2d  19884  dmdprdsplitlem  19951  dprd2dlem1  19955  funcrngcsetc  20555  funcrngcsetcALT  20556  funcringcsetc  20589  psrlidm  21899  psrridm  21900  mplmonmul  21971  mplcoe1  21972  mplcoe5  21975  evlsval2  22022  mdetunilem9  22535  cmpfi  23323  ptpjopn  23527  xkoptsub  23569  xkopjcn  23571  cnmpt1res  23591  subgntr  24022  opnsubg  24023  clsnsg  24025  snclseqg  24031  tsmsxplem1  24068  imasdsf1olem  24288  subgnm  24548  cphsscph  25178  mbfss  25574  mbflimsup  25594  mbfmullem2  25652  iblss  25733  limcres  25814  dvmptresicc  25844  dvaddbr  25867  dvmulbr  25868  dvmulbrOLD  25869  dvcmulf  25875  dvmptres3  25887  dvmptres2  25893  dvmptntr  25902  lhop2  25947  lhop  25948  dvfsumle  25953  dvfsumleOLD  25954  dvfsumabs  25956  dvfsumlem2  25960  dvfsumlem2OLD  25961  ftc2ditglem  25979  itgsubstlem  25982  itgpowd  25984  mdegfval  25994  psercn2  26359  psercn2OLD  26360  psercn  26363  abelth  26378  abelth2  26379  efrlim  26906  efrlimOLD  26907  jensenlem2  26925  lgamcvg2  26992  pntrsumo1  27503  clwlknf1oclwwlknlem3  30063  eucrct2eupth  30225  rabfodom  32485  qusima  33373  elrspunidl  33393  ressply1evls1  33528  poimirlem16  37675  poimirlem19  37678  poimirlem30  37689  ftc1anclem8  37739  ftc2nc  37741  areacirclem2  37748  aks4d1p1p5  42167  aks6d1c6lem2  42263  aks6d1c6lem4  42265  evlsval3  42651  selvvvval  42677  evlselv  42679  evlsmhpvvval  42687  hbtlem6  43221  radcnvrat  44406  disjf1o  45287  cncfmptss  45686  limsupvaluzmpt  45814  supcnvlimsupmpt  45838  dvnprodlem1  46043  iblsplit  46063  itgcoscmulx  46066  itgiccshift  46077  itgperiod  46078  itgsbtaddcnst  46079  dirkercncflem2  46201  dirkercncflem4  46203  fourierdlem28  46232  fourierdlem40  46244  fourierdlem58  46261  fourierdlem74  46277  fourierdlem75  46278  fourierdlem76  46279  fourierdlem78  46281  fourierdlem80  46283  fourierdlem81  46284  fourierdlem84  46287  fourierdlem85  46288  fourierdlem90  46293  fourierdlem93  46296  fourierdlem101  46304  fourierdlem111  46314  sge0lessmpt  46496  sge0gerpmpt  46499  sge0resrnlem  46500  sge0ssrempt  46502  sge0ltfirpmpt  46505  sge0iunmptlemre  46512  sge0lefimpt  46520  sge0ltfirpmpt2  46523  sge0pnffigtmpt  46537  ismeannd  46564  omeiunltfirp  46616  caratheodorylem2  46624  sssmfmpt  46847  gsumsplit2f  48279  fdmdifeqresdif  48441