Theorem resmptd 6047

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ⊆ wss 3908   ↦ cmpt 5197   ↾ cres 5668

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 2148  ax-9 2156  ax-10 2179  ax-12 2216  ax-ext 2738  ax-sep 5262  ax-pr 5409

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 2745  df-cleq 2758  df-clel 2841  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-opab 5179  df-mpt 5198  df-xp 5672  df-rel 5673  df-res 5678

This theorem is used by:  f1ossf1o  7131  oacomf1olem  8558  fmptssfisupp  9364  cantnfres  9656  rlimres2  15638  lo1res2  15639  o1res2  15640  fsumss  15802  fprodss  16028  conjsubgen  19352  gsumsplit2  20030  gsum2d  20073  dmdprdsplitlem  20140  dprd2dlem1  20144  funcrngcsetc  20776  funcrngcsetcALT  20777  funcringcsetc  20810  psrlidm  22148  psrridm  22149  mplmonmul  22224  mplcoe1  22225  mplcoe5  22228  evlsval2  22275  evlsval3  22277  selvvvval  22330  mdetunilem9  22814  cmpfi  23602  ptpjopn  23806  xkoptsub  23848  xkopjcn  23850  cnmpt1res  23870  subgntr  24301  opnsubg  24302  clsnsg  24304  snclseqg  24310  tsmsxplem1  24347  imasdsf1olem  24567  subgnm  24827  cphsscph  25447  mbfss  25842  mbflimsup  25862  mbfmullem2  25920  iblss  26001  limcres  26082  dvmptresicc  26112  dvaddbr  26134  dvmulbr  26135  dvcmulf  26141  dvmptres3  26152  dvmptres2  26158  dvmptntr  26167  lhop2  26211  lhop  26212  dvfsumle  26217  dvfsumabs  26219  dvfsumlem2  26223  ftc2ditglem  26241  itgsubstlem  26244  itgpowd  26246  mdegfval  26256  psercn2  26623  psercn  26626  abelth  26641  abelth2  26642  efrlim  27171  jensenlem2  27189  lgamcvg2  27256  pntrsumo1  27766  clwlknf1oclwwlknlem3  30471  eucrct2eupth  30633  rabfodom  32888  gsummptfsres  33405  qusima  33748  elrspunidl  33767  ressply1evls1  33886  psrmonmul  33971  poimirlem16  38328  poimirlem19  38331  poimirlem30  38342  ftc1anclem8  38392  ftc2nc  38394  areacirclem2  38401  aks4d1p1p5  42883  aks6d1c6lem2  42979  aks6d1c6lem4  42981  evlselv  43362  evlsmhpvvval  43368  hbtlem6  43897  radcnvrat  45065  disjf1o  45950  cncfmptss  46344  limsupvaluzmpt  46472  supcnvlimsupmpt  46496  dvnprodlem1  46701  iblsplit  46721  itgcoscmulx  46724  itgiccshift  46735  itgperiod  46736  itgsbtaddcnst  46737  dirkercncflem2  46859  dirkercncflem4  46861  fourierdlem28  46890  fourierdlem40  46902  fourierdlem58  46919  fourierdlem74  46935  fourierdlem75  46936  fourierdlem76  46937  fourierdlem78  46939  fourierdlem80  46941  fourierdlem81  46942  fourierdlem84  46945  fourierdlem85  46946  fourierdlem90  46951  fourierdlem93  46954  fourierdlem101  46962  fourierdlem111  46972  sge0lessmpt  47154  sge0gerpmpt  47157  sge0resrnlem  47158  sge0ssrempt  47160  sge0ltfirpmpt  47163  sge0iunmptlemre  47170  sge0lefimpt  47178  sge0ltfirpmpt2  47181  sge0pnffigtmpt  47195  ismeannd  47222  omeiunltfirp  47274  caratheodorylem2  47282  sssmfmpt  47505  gsumsplit2f  48986  fdmdifeqresdif  49163