Theorem resmptd 5902

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

Syntax hints:   → wi 4   = wceq 1533   ⊆ wss 3935   ↦ cmpt 5138   ↾ cres 5551

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pr 5321

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4467  df-sn 4561  df-pr 4563  df-op 4567  df-opab 5121  df-mpt 5139  df-xp 5555  df-rel 5556  df-res 5561

This theorem is referenced by:  f1ossf1o  6884  oacomf1olem  8184  cantnfres  9134  rlimres2  14912  lo1res2  14913  o1res2  14914  fsumss  15076  fprodss  15296  conjsubgen  18385  gsumsplit2  19043  gsum2d  19086  dmdprdsplitlem  19153  dprd2dlem1  19157  psrlidm  20177  psrridm  20178  mplmonmul  20239  mplcoe1  20240  mplcoe5  20243  evlsval2  20294  mdetunilem9  21223  cmpfi  22010  ptpjopn  22214  xkoptsub  22256  xkopjcn  22258  cnmpt1res  22278  subgntr  22709  opnsubg  22710  clsnsg  22712  snclseqg  22718  tsmsxplem1  22755  imasdsf1olem  22977  subgnm  23236  cphsscph  23848  mbfss  24241  mbflimsup  24261  mbfmullem2  24319  iblss  24399  limcres  24478  dvaddbr  24529  dvmulbr  24530  dvcmulf  24536  dvmptres3  24547  dvmptres2  24553  dvmptntr  24562  lhop2  24606  lhop  24607  dvfsumle  24612  dvfsumabs  24614  dvfsumlem2  24618  ftc2ditglem  24636  itgsubstlem  24639  mdegfval  24650  psercn2  25005  psercn  25008  abelth  25023  abelth2  25024  efrlim  25541  jensenlem2  25559  lgamcvg2  25626  pntrsumo1  26135  clwlknf1oclwwlknlem3  27856  eucrct2eupth  28018  rabfodom  30260  fmptssfisupp  30422  poimirlem16  34902  poimirlem19  34905  poimirlem30  34916  ftc1anclem8  34968  ftc2nc  34970  areacirclem2  34977  hbtlem6  39722  itgpowd  39814  radcnvrat  40639  disjf1o  41445  cncfmptss  41861  limsupvaluzmpt  41991  supcnvlimsupmpt  42015  dvmptresicc  42197  dvnprodlem1  42224  iblsplit  42244  itgcoscmulx  42247  itgiccshift  42258  itgperiod  42259  itgsbtaddcnst  42260  dirkercncflem2  42383  dirkercncflem4  42385  fourierdlem28  42414  fourierdlem40  42426  fourierdlem58  42443  fourierdlem74  42459  fourierdlem75  42460  fourierdlem76  42461  fourierdlem78  42463  fourierdlem80  42465  fourierdlem81  42466  fourierdlem84  42469  fourierdlem85  42470  fourierdlem90  42475  fourierdlem93  42478  fourierdlem101  42486  fourierdlem111  42496  sge0lessmpt  42675  sge0gerpmpt  42678  sge0resrnlem  42679  sge0ssrempt  42681  sge0ltfirpmpt  42684  sge0iunmptlemre  42691  sge0lefimpt  42699  sge0ltfirpmpt2  42702  sge0pnffigtmpt  42716  ismeannd  42743  omeiunltfirp  42795  caratheodorylem2  42803  sssmfmpt  43021  gsumsplit2f  44081  funcrngcsetc  44263  funcrngcsetcALT  44264  funcringcsetc  44300  fdmdifeqresdif  44384