Theorem resmpt 6066

Description: Restriction of the mapping operation. (Contributed by Mario Carneiro, 15-Jul-2013.)

Assertion

Ref	Expression
resmpt	⊢ (𝐵 ⊆ 𝐴 → ((𝑥 ∈ 𝐴 ↦ 𝐶) ↾ 𝐵) = (𝑥 ∈ 𝐵 ↦ 𝐶))

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Allowed substitution hint:   𝐶(𝑥)

Proof of Theorem resmpt

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		resopab2 6065	. 2 ⊢ (𝐵 ⊆ 𝐴 → ({⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶)} ↾ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐵 ∧ 𝑦 = 𝐶)})
2		df-mpt 5250	. . 3 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐶) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶)}
3	2	reseq1i 6005	. 2 ⊢ ((𝑥 ∈ 𝐴 ↦ 𝐶) ↾ 𝐵) = ({⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶)} ↾ 𝐵)
4		df-mpt 5250	. 2 ⊢ (𝑥 ∈ 𝐵 ↦ 𝐶) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐵 ∧ 𝑦 = 𝐶)}
5	1, 3, 4	3eqtr4g 2805	1 ⊢ (𝐵 ⊆ 𝐴 → ((𝑥 ∈ 𝐴 ↦ 𝐶) ↾ 𝐵) = (𝑥 ∈ 𝐵 ↦ 𝐶))

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1537   ∈ wcel 2108   ⊆ wss 3976  {copab 5228   ↦ 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:  resmpt3  6067  resmptf  6068  resmptd  6069  mptss  6071  elimampt  6072  fvresex  8000  f1stres  8054  f2ndres  8055  tposss  8268  dftpos2  8284  dftpos4  8286  resixpfo  8994  rlimresb  15611  lo1eq  15614  rlimeq  15615  fsumss  15773  isumclim3  15807  divcnvshft  15903  fprodss  15996  iprodclim3  16048  fprodefsum  16143  bitsf1ocnv  16490  conjsubg  19290  odf1o2  19615  sylow1lem2  19641  sylow2blem1  19662  gsumzres  19951  gsumzsplit  19969  gsumpr  19997  gsumzunsnd  19998  gsum2dlem2  20013  gsummptnn0fz  20028  dprd2da  20086  dpjidcl  20102  ablfac1b  20114  frlmsplit2  21816  psrass1lem  21975  coe1mul2lem2  22292  ofco2  22478  mdetralt  22635  mdetunilem9  22647  tgrest  23188  cmpfi  23437  fmss  23975  txflf  24035  tmdgsum  24124  tgpconncomp  24142  tsmssplit  24181  iscmet3lem3  25343  mbfss  25700  mbfadd  25715  mbfsub  25716  mbflimsup  25720  mbfmul  25781  itg2cnlem1  25816  ellimc2  25932  dvreslem  25964  dvres2lem  25965  dvidlem  25970  dvmptresicc  25971  dvcnp2  25975  dvcnp2OLD  25976  dvmulbr  25995  dvmulbrOLD  25996  dvcobr  26003  dvcobrOLD  26004  dvrec  26013  dvmptntr  26029  dvcnvlem  26034  lhop1lem  26072  lhop2  26074  itgparts  26108  itgsubstlem  26109  itgpowd  26111  plypf1  26271  taylthlem2  26434  taylthlem2OLD  26435  pserdvlem2  26490  abelth  26503  pige3ALT  26580  efifo  26607  eff1olem  26608  dvlog2  26713  resqrtcn  26810  sqrtcn  26811  dvatan  26996  rlimcnp2  27027  xrlimcnp  27029  efrlim  27030  efrlimOLD  27031  cxp2lim  27038  chpo1ub  27542  dchrisum0lem2a  27579  pnt2  27675  pnt  27676  wlknwwlksnbij  29921  ressnm  32931  gsummpt2d  33032  rmulccn  33874  xrge0mulc1cn  33887  gsumesum  34023  esumsnf  34028  esumcvg  34050  omsmon  34263  carsggect  34283  eulerpartlem1  34332  eulerpartgbij  34337  gsumnunsn  34518  cxpcncf1  34572  itgexpif  34583  reprpmtf1o  34603  elmsubrn  35496  divcnvlin  35695  mptsnunlem  37304  dissneqlem  37306  broucube  37614  mbfposadd  37627  itggt0cn  37650  ftc1anclem3  37655  ftc1anclem8  37660  dvasin  37664  dvacos  37665  areacirc  37673  sdclem2  37702  cncfres  37725  resopunitintvd  41983  resclunitintvd  41984  lcmineqlem2  41987  evlsbagval  42521  pwssplit4  43046  pwfi2f1o  43053  hbtlem6  43086  areaquad  43177  hashnzfzclim  44291  lhe4.4ex1a  44298  resmpti  45085  climresmpt  45580  dvcosre  45833  itgsinexplem1  45875  itgcoscmulx  45890  dirkeritg  46023  dirkercncflem2  46025  fourierdlem16  46044  fourierdlem21  46049  fourierdlem22  46050  fourierdlem57  46084  fourierdlem58  46085  fourierdlem62  46089  fourierdlem83  46110  fourierdlem111  46138  fouriersw  46152  0ome  46450