Theorem resmptd 6045

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

Syntax hints:   → wi 4   = wceq 1567   ⊆ wss 3913   ↦ cmpt 5196   ↾ cres 5666

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-12 2219  ax-ext 2741  ax-sep 5261  ax-pr 5407

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-opab 5178  df-mpt 5197  df-xp 5670  df-rel 5671  df-res 5676

This theorem is referenced by:  f1ossf1o  7127  oacomf1olem  8551  fmptssfisupp  9356  cantnfres  9648  rlimres2  15614  lo1res2  15615  o1res2  15616  fsumss  15778  fprodss  16004  conjsubgen  19323  gsumsplit2  20001  gsum2d  20044  dmdprdsplitlem  20111  dprd2dlem1  20115  funcrngcsetc  20727  funcrngcsetcALT  20728  funcringcsetc  20761  psrlidm  22082  psrridm  22083  mplmonmul  22158  mplcoe1  22159  mplcoe5  22162  evlsval2  22209  evlsval3  22211  selvvvval  22264  mdetunilem9  22748  cmpfi  23536  ptpjopn  23740  xkoptsub  23782  xkopjcn  23784  cnmpt1res  23804  subgntr  24235  opnsubg  24236  clsnsg  24238  snclseqg  24244  tsmsxplem1  24281  imasdsf1olem  24501  subgnm  24761  cphsscph  25381  mbfss  25776  mbflimsup  25796  mbfmullem2  25854  iblss  25935  limcres  26016  dvmptresicc  26046  dvaddbr  26068  dvmulbr  26069  dvcmulf  26075  dvmptres3  26086  dvmptres2  26092  dvmptntr  26101  lhop2  26145  lhop  26146  dvfsumle  26151  dvfsumabs  26153  dvfsumlem2  26157  ftc2ditglem  26175  itgsubstlem  26178  itgpowd  26180  mdegfval  26190  psercn2  26554  psercn  26557  abelth  26572  abelth2  26573  efrlim  27102  jensenlem2  27120  lgamcvg2  27187  pntrsumo1  27697  clwlknf1oclwwlknlem3  30377  eucrct2eupth  30539  rabfodom  32794  gsummptfsres  33317  qusima  33663  elrspunidl  33682  ressply1evls1  33802  psrmonmul  33887  poimirlem16  38212  poimirlem19  38215  poimirlem30  38226  ftc1anclem8  38276  ftc2nc  38278  areacirclem2  38285  aks4d1p1p5  42769  aks6d1c6lem2  42865  aks6d1c6lem4  42867  evlselv  43250  evlsmhpvvval  43256  hbtlem6  43785  radcnvrat  44953  disjf1o  45838  cncfmptss  46232  limsupvaluzmpt  46360  supcnvlimsupmpt  46384  dvnprodlem1  46589  iblsplit  46609  itgcoscmulx  46612  itgiccshift  46623  itgperiod  46624  itgsbtaddcnst  46625  dirkercncflem2  46747  dirkercncflem4  46749  fourierdlem28  46778  fourierdlem40  46790  fourierdlem58  46807  fourierdlem74  46823  fourierdlem75  46824  fourierdlem76  46825  fourierdlem78  46827  fourierdlem80  46829  fourierdlem81  46830  fourierdlem84  46833  fourierdlem85  46834  fourierdlem90  46839  fourierdlem93  46842  fourierdlem101  46850  fourierdlem111  46860  sge0lessmpt  47042  sge0gerpmpt  47045  sge0resrnlem  47046  sge0ssrempt  47048  sge0ltfirpmpt  47051  sge0iunmptlemre  47058  sge0lefimpt  47066  sge0ltfirpmpt2  47069  sge0pnffigtmpt  47083  ismeannd  47110  omeiunltfirp  47162  caratheodorylem2  47170  sssmfmpt  47393  gsumsplit2f  48871  fdmdifeqresdif  49044