Theorem resmptd 5995

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

Syntax hints:   → wi 4   = wceq 1540   ⊆ wss 3905   ↦ cmpt 5176   ↾ cres 5625

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 2701  ax-sep 5238  ax-nul 5248  ax-pr 5374

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 2708  df-cleq 2721  df-clel 2803  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-opab 5158  df-mpt 5177  df-xp 5629  df-rel 5630  df-res 5635

This theorem is referenced by:  f1ossf1o  7066  oacomf1olem  8489  fmptssfisupp  9303  cantnfres  9592  rlimres2  15486  lo1res2  15487  o1res2  15488  fsumss  15650  fprodss  15873  conjsubgen  19148  gsumsplit2  19826  gsum2d  19869  dmdprdsplitlem  19936  dprd2dlem1  19940  funcrngcsetc  20543  funcrngcsetcALT  20544  funcringcsetc  20577  psrlidm  21887  psrridm  21888  mplmonmul  21959  mplcoe1  21960  mplcoe5  21963  evlsval2  22010  mdetunilem9  22523  cmpfi  23311  ptpjopn  23515  xkoptsub  23557  xkopjcn  23559  cnmpt1res  23579  subgntr  24010  opnsubg  24011  clsnsg  24013  snclseqg  24019  tsmsxplem1  24056  imasdsf1olem  24277  subgnm  24537  cphsscph  25167  mbfss  25563  mbflimsup  25583  mbfmullem2  25641  iblss  25722  limcres  25803  dvmptresicc  25833  dvaddbr  25856  dvmulbr  25857  dvmulbrOLD  25858  dvcmulf  25864  dvmptres3  25876  dvmptres2  25882  dvmptntr  25891  lhop2  25936  lhop  25937  dvfsumle  25942  dvfsumleOLD  25943  dvfsumabs  25945  dvfsumlem2  25949  dvfsumlem2OLD  25950  ftc2ditglem  25968  itgsubstlem  25971  itgpowd  25973  mdegfval  25983  psercn2  26348  psercn2OLD  26349  psercn  26352  abelth  26367  abelth2  26368  efrlim  26895  efrlimOLD  26896  jensenlem2  26914  lgamcvg2  26981  pntrsumo1  27492  clwlknf1oclwwlknlem3  30045  eucrct2eupth  30207  rabfodom  32467  qusima  33358  elrspunidl  33378  ressply1evls1  33513  poimirlem16  37618  poimirlem19  37621  poimirlem30  37632  ftc1anclem8  37682  ftc2nc  37684  areacirclem2  37691  aks4d1p1p5  42051  aks6d1c6lem2  42147  aks6d1c6lem4  42149  evlsval3  42535  selvvvval  42561  evlselv  42563  evlsmhpvvval  42571  hbtlem6  43105  radcnvrat  44290  disjf1o  45172  cncfmptss  45572  limsupvaluzmpt  45702  supcnvlimsupmpt  45726  dvnprodlem1  45931  iblsplit  45951  itgcoscmulx  45954  itgiccshift  45965  itgperiod  45966  itgsbtaddcnst  45967  dirkercncflem2  46089  dirkercncflem4  46091  fourierdlem28  46120  fourierdlem40  46132  fourierdlem58  46149  fourierdlem74  46165  fourierdlem75  46166  fourierdlem76  46167  fourierdlem78  46169  fourierdlem80  46171  fourierdlem81  46172  fourierdlem84  46175  fourierdlem85  46176  fourierdlem90  46181  fourierdlem93  46184  fourierdlem101  46192  fourierdlem111  46202  sge0lessmpt  46384  sge0gerpmpt  46387  sge0resrnlem  46388  sge0ssrempt  46390  sge0ltfirpmpt  46393  sge0iunmptlemre  46400  sge0lefimpt  46408  sge0ltfirpmpt2  46411  sge0pnffigtmpt  46425  ismeannd  46452  omeiunltfirp  46504  caratheodorylem2  46512  sssmfmpt  46735  gsumsplit2f  48168  fdmdifeqresdif  48330