Theorem resmptd 6044

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ⊆ wss 3900   ↦ cmpt 5189   ↾ cres 5657

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-12 2216  ax-ext 2735  ax-sep 5252  ax-pr 5395

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-opab 5171  df-mpt 5190  df-xp 5661  df-rel 5662  df-res 5667

This theorem is used by:  f1ossf1o  7153  oacomf1olem  8600  fmptssfisupp  9413  cantnfres  9705  rlimres2  15757  lo1res2  15758  o1res2  15759  fsumss  15920  fprodss  16144  conjsubgen  19494  gsumsplit2  20173  gsum2d  20216  dmdprdsplitlem  20283  dprd2dlem1  20287  funcrngcsetc  20922  funcrngcsetcALT  20923  funcringcsetc  20956  psrlidm  22299  psrridm  22300  mplmonmul  22375  mplcoe1  22376  mplcoe5  22379  evlsval2  22426  evlsval3  22428  selvvvval  22481  mdetunilem9  22965  cmpfi  23756  ptpjopn  23961  xkoptsub  24003  xkopjcn  24005  cnmpt1res  24025  subgntr  24456  opnsubg  24457  clsnsg  24459  snclseqg  24465  tsmsxplem1  24502  imasdsf1olem  24722  subgnm  24982  cphsscph  25602  mbfss  25997  mbflimsup  26017  mbfmullem2  26075  iblss  26155  limcres  26236  dvmptresicc  26266  dvaddbr  26288  dvmulbr  26289  dvcmulf  26295  dvmptres3  26306  dvmptres2  26312  dvmptntr  26321  lhop2  26365  lhop  26366  dvfsumle  26371  dvfsumabs  26373  dvfsumlem2  26377  ftc2ditglem  26395  itgsubstlem  26398  itgpowd  26400  mdegfval  26410  psercn2  26780  psercn  26783  abelth  26798  abelth2  26799  efrlim  27327  jensenlem2  27345  lgamcvg2  27412  pntrsumo1  27922  clwlknf1oclwwlknlem3  30704  eucrct2eupth  30876  rabfodom  33173  gsummptfsres  33685  qusima  34029  elrspunidl  34048  ressply1evls1  34167  psrmonmul  34252  poimirlem16  38746  poimirlem19  38749  poimirlem30  38760  ftc1anclem8  38810  ftc2nc  38812  areacirclem2  38819  aks4d1p1p5  43317  aks6d1c6lem2  43413  aks6d1c6lem4  43415  evlselv  43810  evlsmhpvvval  43816  hbtlem6  44323  radcnvrat  45490  disjf1o  46411  cncfmptss  46804  limsupvaluzmpt  46932  supcnvlimsupmpt  46956  dvnprodlem1  47161  iblsplit  47181  itgcoscmulx  47184  itgiccshift  47195  itgperiod  47196  itgsbtaddcnst  47197  dirkercncflem2  47319  dirkercncflem4  47321  fourierdlem28  47350  fourierdlem40  47362  fourierdlem58  47379  fourierdlem74  47395  fourierdlem75  47396  fourierdlem76  47397  fourierdlem78  47399  fourierdlem80  47401  fourierdlem81  47402  fourierdlem84  47405  fourierdlem85  47406  fourierdlem90  47411  fourierdlem93  47414  fourierdlem101  47422  fourierdlem111  47432  sge0lessmpt  47614  sge0gerpmpt  47617  sge0resrnlem  47618  sge0ssrempt  47620  sge0ltfirpmpt  47623  sge0iunmptlemre  47630  sge0lefimpt  47638  sge0ltfirpmpt2  47641  sge0pnffigtmpt  47655  ismeannd  47682  omeiunltfirp  47734  caratheodorylem2  47742  sssmfmpt  47965  gsumsplit2f  49482  fdmdifeqresdif  49659