Theorem resmptd 5910

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

Syntax hints:   → wi 4   = wceq 1537   ⊆ wss 3938   ↦ cmpt 5148   ↾ cres 5559

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205  ax-nul 5212  ax-pr 5332

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-rab 3149  df-v 3498  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-sn 4570  df-pr 4572  df-op 4576  df-opab 5131  df-mpt 5149  df-xp 5563  df-rel 5564  df-res 5569

This theorem is referenced by:  f1ossf1o  6892  oacomf1olem  8192  cantnfres  9142  rlimres2  14920  lo1res2  14921  o1res2  14922  fsumss  15084  fprodss  15304  conjsubgen  18393  gsumsplit2  19051  gsum2d  19094  dmdprdsplitlem  19161  dprd2dlem1  19165  psrlidm  20185  psrridm  20186  mplmonmul  20247  mplcoe1  20248  mplcoe5  20251  evlsval2  20302  mdetunilem9  21231  cmpfi  22018  ptpjopn  22222  xkoptsub  22264  xkopjcn  22266  cnmpt1res  22286  subgntr  22717  opnsubg  22718  clsnsg  22720  snclseqg  22726  tsmsxplem1  22763  imasdsf1olem  22985  subgnm  23244  cphsscph  23856  mbfss  24249  mbflimsup  24269  mbfmullem2  24327  iblss  24407  limcres  24486  dvaddbr  24537  dvmulbr  24538  dvcmulf  24544  dvmptres3  24555  dvmptres2  24561  dvmptntr  24570  lhop2  24614  lhop  24615  dvfsumle  24620  dvfsumabs  24622  dvfsumlem2  24626  ftc2ditglem  24644  itgsubstlem  24647  mdegfval  24658  psercn2  25013  psercn  25016  abelth  25031  abelth2  25032  efrlim  25549  jensenlem2  25567  lgamcvg2  25634  pntrsumo1  26143  clwlknf1oclwwlknlem3  27864  eucrct2eupth  28026  rabfodom  30268  fmptssfisupp  30430  poimirlem16  34910  poimirlem19  34913  poimirlem30  34924  ftc1anclem8  34976  ftc2nc  34978  areacirclem2  34985  hbtlem6  39736  itgpowd  39828  radcnvrat  40653  disjf1o  41459  cncfmptss  41875  limsupvaluzmpt  42005  supcnvlimsupmpt  42029  dvmptresicc  42211  dvnprodlem1  42238  iblsplit  42258  itgcoscmulx  42261  itgiccshift  42272  itgperiod  42273  itgsbtaddcnst  42274  dirkercncflem2  42396  dirkercncflem4  42398  fourierdlem28  42427  fourierdlem40  42439  fourierdlem58  42456  fourierdlem74  42472  fourierdlem75  42473  fourierdlem76  42474  fourierdlem78  42476  fourierdlem80  42478  fourierdlem81  42479  fourierdlem84  42482  fourierdlem85  42483  fourierdlem90  42488  fourierdlem93  42491  fourierdlem101  42499  fourierdlem111  42509  sge0lessmpt  42688  sge0gerpmpt  42691  sge0resrnlem  42692  sge0ssrempt  42694  sge0ltfirpmpt  42697  sge0iunmptlemre  42704  sge0lefimpt  42712  sge0ltfirpmpt2  42715  sge0pnffigtmpt  42729  ismeannd  42756  omeiunltfirp  42808  caratheodorylem2  42816  sssmfmpt  43034  gsumsplit2f  44094  funcrngcsetc  44276  funcrngcsetcALT  44277  funcringcsetc  44313  fdmdifeqresdif  44397