Theorem resmptd 6069

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

Syntax hints:   → wi 4   = wceq 1537   ⊆ wss 3976   ↦ cmpt 5249   ↾ cres 5702

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-opab 5229  df-mpt 5250  df-xp 5706  df-rel 5707  df-res 5712

This theorem is referenced by:  f1ossf1o  7162  oacomf1olem  8620  fmptssfisupp  9463  cantnfres  9746  rlimres2  15607  lo1res2  15608  o1res2  15609  fsumss  15773  fprodss  15996  conjsubgen  19291  gsumsplit2  19971  gsum2d  20014  dmdprdsplitlem  20081  dprd2dlem1  20085  funcrngcsetc  20662  funcrngcsetcALT  20663  funcringcsetc  20696  psrlidm  22005  psrridm  22006  mplmonmul  22077  mplcoe1  22078  mplcoe5  22081  evlsval2  22134  mdetunilem9  22647  cmpfi  23437  ptpjopn  23641  xkoptsub  23683  xkopjcn  23685  cnmpt1res  23705  subgntr  24136  opnsubg  24137  clsnsg  24139  snclseqg  24145  tsmsxplem1  24182  imasdsf1olem  24404  subgnm  24667  cphsscph  25304  mbfss  25700  mbflimsup  25720  mbfmullem2  25779  iblss  25860  limcres  25941  dvmptresicc  25971  dvaddbr  25994  dvmulbr  25995  dvmulbrOLD  25996  dvcmulf  26002  dvmptres3  26014  dvmptres2  26020  dvmptntr  26029  lhop2  26074  lhop  26075  dvfsumle  26080  dvfsumleOLD  26081  dvfsumabs  26083  dvfsumlem2  26087  dvfsumlem2OLD  26088  ftc2ditglem  26106  itgsubstlem  26109  itgpowd  26111  mdegfval  26121  psercn2  26484  psercn2OLD  26485  psercn  26488  abelth  26503  abelth2  26504  efrlim  27030  efrlimOLD  27031  jensenlem2  27049  lgamcvg2  27116  pntrsumo1  27627  clwlknf1oclwwlknlem3  30115  eucrct2eupth  30277  rabfodom  32533  qusima  33401  elrspunidl  33421  poimirlem16  37596  poimirlem19  37599  poimirlem30  37610  ftc1anclem8  37660  ftc2nc  37662  areacirclem2  37669  aks4d1p1p5  42032  aks6d1c6lem2  42128  aks6d1c6lem4  42130  evlsval3  42514  selvvvval  42540  evlselv  42542  evlsmhpvvval  42550  hbtlem6  43086  radcnvrat  44283  disjf1o  45098  cncfmptss  45508  limsupvaluzmpt  45638  supcnvlimsupmpt  45662  dvnprodlem1  45867  iblsplit  45887  itgcoscmulx  45890  itgiccshift  45901  itgperiod  45902  itgsbtaddcnst  45903  dirkercncflem2  46025  dirkercncflem4  46027  fourierdlem28  46056  fourierdlem40  46068  fourierdlem58  46085  fourierdlem74  46101  fourierdlem75  46102  fourierdlem76  46103  fourierdlem78  46105  fourierdlem80  46107  fourierdlem81  46108  fourierdlem84  46111  fourierdlem85  46112  fourierdlem90  46117  fourierdlem93  46120  fourierdlem101  46128  fourierdlem111  46138  sge0lessmpt  46320  sge0gerpmpt  46323  sge0resrnlem  46324  sge0ssrempt  46326  sge0ltfirpmpt  46329  sge0iunmptlemre  46336  sge0lefimpt  46344  sge0ltfirpmpt2  46347  sge0pnffigtmpt  46361  ismeannd  46388  omeiunltfirp  46440  caratheodorylem2  46448  sssmfmpt  46671  gsumsplit2f  47903  fdmdifeqresdif  48066