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 18	1 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐶) ↾ 𝐵) = (𝑥 ∈ 𝐵 ↦ 𝐶))

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ⊆ wss 3902   ↦ cmpt 5190   ↾ cres 5661

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-pr 5402

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-opab 5172  df-mpt 5191  df-xp 5665  df-rel 5666  df-res 5671

This theorem is used by:  f1ossf1o  7126  oacomf1olem  8555  fmptssfisupp  9368  cantnfres  9660  rlimres2  15652  lo1res2  15653  o1res2  15654  fsumss  15815  fprodss  16041  conjsubgen  19384  gsumsplit2  20062  gsum2d  20105  dmdprdsplitlem  20172  dprd2dlem1  20176  funcrngcsetc  20808  funcrngcsetcALT  20809  funcringcsetc  20842  psrlidm  22182  psrridm  22183  mplmonmul  22258  mplcoe1  22259  mplcoe5  22262  evlsval2  22309  evlsval3  22311  selvvvval  22364  mdetunilem9  22848  cmpfi  23639  ptpjopn  23844  xkoptsub  23886  xkopjcn  23888  cnmpt1res  23908  subgntr  24339  opnsubg  24340  clsnsg  24342  snclseqg  24348  tsmsxplem1  24385  imasdsf1olem  24605  subgnm  24865  cphsscph  25485  mbfss  25880  mbflimsup  25900  mbfmullem2  25958  iblss  26039  limcres  26120  dvmptresicc  26150  dvaddbr  26172  dvmulbr  26173  dvcmulf  26179  dvmptres3  26190  dvmptres2  26196  dvmptntr  26205  lhop2  26249  lhop  26250  dvfsumle  26255  dvfsumabs  26257  dvfsumlem2  26261  ftc2ditglem  26279  itgsubstlem  26282  itgpowd  26284  mdegfval  26294  psercn2  26666  psercn  26669  abelth  26684  abelth2  26685  efrlim  27214  jensenlem2  27232  lgamcvg2  27299  pntrsumo1  27809  clwlknf1oclwwlknlem3  30561  eucrct2eupth  30733  rabfodom  32988  gsummptfsres  33502  qusima  33845  elrspunidl  33864  ressply1evls1  33983  psrmonmul  34068  poimirlem16  38393  poimirlem19  38396  poimirlem30  38407  ftc1anclem8  38457  ftc2nc  38459  areacirclem2  38466  aks4d1p1p5  42949  aks6d1c6lem2  43045  aks6d1c6lem4  43047  evlselv  43443  evlsmhpvvval  43449  hbtlem6  43978  radcnvrat  45146  disjf1o  46031  cncfmptss  46425  limsupvaluzmpt  46553  supcnvlimsupmpt  46577  dvnprodlem1  46782  iblsplit  46802  itgcoscmulx  46805  itgiccshift  46816  itgperiod  46817  itgsbtaddcnst  46818  dirkercncflem2  46940  dirkercncflem4  46942  fourierdlem28  46971  fourierdlem40  46983  fourierdlem58  47000  fourierdlem74  47016  fourierdlem75  47017  fourierdlem76  47018  fourierdlem78  47020  fourierdlem80  47022  fourierdlem81  47023  fourierdlem84  47026  fourierdlem85  47027  fourierdlem90  47032  fourierdlem93  47035  fourierdlem101  47043  fourierdlem111  47053  sge0lessmpt  47235  sge0gerpmpt  47238  sge0resrnlem  47239  sge0ssrempt  47241  sge0ltfirpmpt  47244  sge0iunmptlemre  47251  sge0lefimpt  47259  sge0ltfirpmpt2  47262  sge0pnffigtmpt  47276  ismeannd  47303  omeiunltfirp  47355  caratheodorylem2  47363  sssmfmpt  47586  gsumsplit2f  49103  fdmdifeqresdif  49280