Theorem resmptd 6034

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ⊆ wss 3899   ↦ cmpt 5186   ↾ cres 5653

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 2213  ax-ext 2733  ax-sep 5249  ax-pr 5391

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 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-opab 5168  df-mpt 5187  df-xp 5657  df-rel 5658  df-res 5663

This theorem is used by:  f1ossf1o  7121  oacomf1olem  8556  fmptssfisupp  9370  cantnfres  9662  rlimres2  15708  lo1res2  15709  o1res2  15710  fsumss  15871  fprodss  16095  conjsubgen  19445  gsumsplit2  20123  gsum2d  20166  dmdprdsplitlem  20233  dprd2dlem1  20237  funcrngcsetc  20872  funcrngcsetcALT  20873  funcringcsetc  20906  psrlidm  22249  psrridm  22250  mplmonmul  22325  mplcoe1  22326  mplcoe5  22329  evlsval2  22376  evlsval3  22378  selvvvval  22431  mdetunilem9  22915  cmpfi  23706  ptpjopn  23911  xkoptsub  23953  xkopjcn  23955  cnmpt1res  23975  subgntr  24406  opnsubg  24407  clsnsg  24409  snclseqg  24415  tsmsxplem1  24452  imasdsf1olem  24672  subgnm  24932  cphsscph  25552  mbfss  25947  mbflimsup  25967  mbfmullem2  26025  iblss  26105  limcres  26186  dvmptresicc  26216  dvaddbr  26238  dvmulbr  26239  dvcmulf  26245  dvmptres3  26256  dvmptres2  26262  dvmptntr  26271  lhop2  26315  lhop  26316  dvfsumle  26321  dvfsumabs  26323  dvfsumlem2  26327  ftc2ditglem  26345  itgsubstlem  26348  itgpowd  26350  mdegfval  26360  psercn2  26732  psercn  26735  abelth  26750  abelth2  26751  efrlim  27279  jensenlem2  27297  lgamcvg2  27364  pntrsumo1  27874  clwlknf1oclwwlknlem3  30656  eucrct2eupth  30828  rabfodom  33083  gsummptfsres  33597  qusima  33941  elrspunidl  33960  ressply1evls1  34079  psrmonmul  34164  poimirlem16  38522  poimirlem19  38525  poimirlem30  38536  ftc1anclem8  38586  ftc2nc  38588  areacirclem2  38595  aks4d1p1p5  43093  aks6d1c6lem2  43189  aks6d1c6lem4  43191  evlselv  43579  evlsmhpvvval  43585  hbtlem6  44089  radcnvrat  45257  disjf1o  46149  cncfmptss  46543  limsupvaluzmpt  46671  supcnvlimsupmpt  46695  dvnprodlem1  46900  iblsplit  46920  itgcoscmulx  46923  itgiccshift  46934  itgperiod  46935  itgsbtaddcnst  46936  dirkercncflem2  47058  dirkercncflem4  47060  fourierdlem28  47089  fourierdlem40  47101  fourierdlem58  47118  fourierdlem74  47134  fourierdlem75  47135  fourierdlem76  47136  fourierdlem78  47138  fourierdlem80  47140  fourierdlem81  47141  fourierdlem84  47144  fourierdlem85  47145  fourierdlem90  47150  fourierdlem93  47153  fourierdlem101  47161  fourierdlem111  47171  sge0lessmpt  47353  sge0gerpmpt  47356  sge0resrnlem  47357  sge0ssrempt  47359  sge0ltfirpmpt  47362  sge0iunmptlemre  47369  sge0lefimpt  47377  sge0ltfirpmpt2  47380  sge0pnffigtmpt  47394  ismeannd  47421  omeiunltfirp  47473  caratheodorylem2  47481  sssmfmpt  47704  gsumsplit2f  49221  fdmdifeqresdif  49398