Theorem resmptd 6014

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

Syntax hints:   → wi 4   = wceq 1540   ⊆ wss 3917   ↦ cmpt 5191   ↾ cres 5643

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-opab 5173  df-mpt 5192  df-xp 5647  df-rel 5648  df-res 5653

This theorem is referenced by:  f1ossf1o  7103  oacomf1olem  8531  fmptssfisupp  9352  cantnfres  9637  rlimres2  15534  lo1res2  15535  o1res2  15536  fsumss  15698  fprodss  15921  conjsubgen  19190  gsumsplit2  19866  gsum2d  19909  dmdprdsplitlem  19976  dprd2dlem1  19980  funcrngcsetc  20556  funcrngcsetcALT  20557  funcringcsetc  20590  psrlidm  21878  psrridm  21879  mplmonmul  21950  mplcoe1  21951  mplcoe5  21954  evlsval2  22001  mdetunilem9  22514  cmpfi  23302  ptpjopn  23506  xkoptsub  23548  xkopjcn  23550  cnmpt1res  23570  subgntr  24001  opnsubg  24002  clsnsg  24004  snclseqg  24010  tsmsxplem1  24047  imasdsf1olem  24268  subgnm  24528  cphsscph  25158  mbfss  25554  mbflimsup  25574  mbfmullem2  25632  iblss  25713  limcres  25794  dvmptresicc  25824  dvaddbr  25847  dvmulbr  25848  dvmulbrOLD  25849  dvcmulf  25855  dvmptres3  25867  dvmptres2  25873  dvmptntr  25882  lhop2  25927  lhop  25928  dvfsumle  25933  dvfsumleOLD  25934  dvfsumabs  25936  dvfsumlem2  25940  dvfsumlem2OLD  25941  ftc2ditglem  25959  itgsubstlem  25962  itgpowd  25964  mdegfval  25974  psercn2  26339  psercn2OLD  26340  psercn  26343  abelth  26358  abelth2  26359  efrlim  26886  efrlimOLD  26887  jensenlem2  26905  lgamcvg2  26972  pntrsumo1  27483  clwlknf1oclwwlknlem3  30019  eucrct2eupth  30181  rabfodom  32441  qusima  33386  elrspunidl  33406  ressply1evls1  33541  poimirlem16  37637  poimirlem19  37640  poimirlem30  37651  ftc1anclem8  37701  ftc2nc  37703  areacirclem2  37710  aks4d1p1p5  42070  aks6d1c6lem2  42166  aks6d1c6lem4  42168  evlsval3  42554  selvvvval  42580  evlselv  42582  evlsmhpvvval  42590  hbtlem6  43125  radcnvrat  44310  disjf1o  45192  cncfmptss  45592  limsupvaluzmpt  45722  supcnvlimsupmpt  45746  dvnprodlem1  45951  iblsplit  45971  itgcoscmulx  45974  itgiccshift  45985  itgperiod  45986  itgsbtaddcnst  45987  dirkercncflem2  46109  dirkercncflem4  46111  fourierdlem28  46140  fourierdlem40  46152  fourierdlem58  46169  fourierdlem74  46185  fourierdlem75  46186  fourierdlem76  46187  fourierdlem78  46189  fourierdlem80  46191  fourierdlem81  46192  fourierdlem84  46195  fourierdlem85  46196  fourierdlem90  46201  fourierdlem93  46204  fourierdlem101  46212  fourierdlem111  46222  sge0lessmpt  46404  sge0gerpmpt  46407  sge0resrnlem  46408  sge0ssrempt  46410  sge0ltfirpmpt  46413  sge0iunmptlemre  46420  sge0lefimpt  46428  sge0ltfirpmpt2  46431  sge0pnffigtmpt  46445  ismeannd  46472  omeiunltfirp  46524  caratheodorylem2  46532  sssmfmpt  46755  gsumsplit2f  48172  fdmdifeqresdif  48334