Theorem resmpt 6030

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 6029	. 2 ⊢ (𝐵 ⊆ 𝐴 → ({⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶)} ↾ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐵 ∧ 𝑦 = 𝐶)})
2		df-mpt 5187	. . 3 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐶) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶)}
3	2	reseq1i 5965	. 2 ⊢ ((𝑥 ∈ 𝐴 ↦ 𝐶) ↾ 𝐵) = ({⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶)} ↾ 𝐵)
4		df-mpt 5187	. 2 ⊢ (𝑥 ∈ 𝐵 ↦ 𝐶) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐵 ∧ 𝑦 = 𝐶)}
5	1, 3, 4	3eqtr4g 2825	1 ⊢ (𝐵 ⊆ 𝐴 → ((𝑥 ∈ 𝐴 ↦ 𝐶) ↾ 𝐵) = (𝑥 ∈ 𝐵 ↦ 𝐶))

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1563   ∈ wcel 2145   ⊆ wss 3907  {copab 5167   ↦ cmpt 5186   ↾ cres 5654

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-12 2215  ax-ext 2737  ax-sep 5251  ax-pr 5395

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-opab 5168  df-mpt 5187  df-xp 5658  df-rel 5659  df-res 5664

This theorem is referenced by:  resmpt3  6031  resmptf  6032  resmptd  6033  mptss  6035  elimampt  6036  fvresex  7945  f1stres  7998  f2ndres  7999  tposss  8211  dftpos2  8227  dftpos4  8229  resixpfo  8922  rlimresb  15606  lo1eq  15609  rlimeq  15610  fsumss  15766  isumclim3  15800  divcnvshft  15899  fprodss  15992  iprodclim3  16044  fprodefsum  16139  bitsf1ocnv  16492  conjsubg  19311  odf1o2  19634  sylow1lem2  19660  sylow2blem1  19681  gsumzres  19970  gsumzsplit  19988  gsumpr  20016  gsumzunsnd  20017  gsum2dlem2  20032  gsummptnn0fz  20047  dprd2da  20105  dpjidcl  20121  ablfac1b  20133  frlmsplit2  21883  psrass1lem  22043  coe1mul2lem2  22389  ofco2  22569  mdetralt  22726  mdetunilem9  22738  tgrest  23277  cmpfi  23526  fmss  24064  txflf  24124  tmdgsum  24213  tgpconncomp  24231  tsmssplit  24270  iscmet3lem3  25410  mbfss  25766  mbfadd  25781  mbfsub  25782  mbflimsup  25786  mbfmul  25846  itg2cnlem1  25881  ellimc2  25997  dvreslem  26029  dvres2lem  26030  dvidlem  26035  dvmptresicc  26036  dvcnp2  26040  dvmulbr  26059  dvcobr  26066  dvrec  26075  dvmptntr  26091  dvcnvlem  26096  lhop1lem  26133  lhop2  26135  itgparts  26167  itgsubstlem  26168  itgpowd  26170  plypf1  26330  taylthlem2  26495  pserdvlem2  26549  abelth  26562  pige3ALT  26643  efifo  26670  eff1olem  26671  dvlog2  26776  resqrtcn  26872  sqrtcn  26873  dvatan  27058  rlimcnp2  27089  xrlimcnp  27091  efrlim  27092  cxp2lim  27099  chpo1ub  27602  dchrisum0lem2a  27639  pnt2  27735  pnt  27736  wlknwwlksnbij  30146  ressnm  33197  gsummpt2d  33282  rmulccn  34235  xrge0mulc1cn  34248  gsumesum  34366  esumsnf  34371  esumcvg  34393  omsmon  34605  carsggect  34625  eulerpartlem1  34674  eulerpartgbij  34679  gsumnunsn  34848  cxpcncf1  34899  itgexpif  34910  reprpmtf1o  34930  elmsubrn  35891  divcnvlin  36096  mptsnunlem  37844  dissneqlem  37846  broucube  38165  mbfposadd  38178  itggt0cn  38201  ftc1anclem3  38206  ftc1anclem8  38211  dvasin  38215  dvacos  38216  areacirc  38224  sdclem2  38253  cncfres  38276  resopunitintvd  42655  resclunitintvd  42656  lcmineqlem2  42659  evlsbagval  43180  pwssplit4  43678  pwfi2f1o  43685  hbtlem6  43718  areaquad  43805  hashnzfzclim  44896  lhe4.4ex1a  44903  resmpti  45754  climresmpt  46231  dvcosre  46484  itgsinexplem1  46526  itgcoscmulx  46541  dirkeritg  46674  dirkercncflem2  46676  fourierdlem16  46695  fourierdlem21  46700  fourierdlem22  46701  fourierdlem57  46735  fourierdlem58  46736  fourierdlem62  46740  fourierdlem83  46761  fourierdlem111  46789  fouriersw  46803  0ome  47101