Theorem resmpt 5986

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2111   ⊆ wss 3902  {copab 5153   ↦ cmpt 5172   ↾ cres 5618

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-12 2180  ax-ext 2703  ax-sep 5234  ax-nul 5244  ax-pr 5370

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4476  df-sn 4577  df-pr 4579  df-op 4583  df-opab 5154  df-mpt 5173  df-xp 5622  df-rel 5623  df-res 5628

This theorem is referenced by:  resmpt3  5987  resmptf  5988  resmptd  5989  mptss  5991  elimampt  5992  fvresex  7892  f1stres  7945  f2ndres  7946  tposss  8157  dftpos2  8173  dftpos4  8175  resixpfo  8860  rlimresb  15469  lo1eq  15472  rlimeq  15473  fsumss  15629  isumclim3  15663  divcnvshft  15759  fprodss  15852  iprodclim3  15904  fprodefsum  15999  bitsf1ocnv  16352  conjsubg  19160  odf1o2  19483  sylow1lem2  19509  sylow2blem1  19530  gsumzres  19819  gsumzsplit  19837  gsumpr  19865  gsumzunsnd  19866  gsum2dlem2  19881  gsummptnn0fz  19896  dprd2da  19954  dpjidcl  19970  ablfac1b  19982  frlmsplit2  21708  psrass1lem  21867  coe1mul2lem2  22180  ofco2  22364  mdetralt  22521  mdetunilem9  22533  tgrest  23072  cmpfi  23321  fmss  23859  txflf  23919  tmdgsum  24008  tgpconncomp  24026  tsmssplit  24065  iscmet3lem3  25215  mbfss  25572  mbfadd  25587  mbfsub  25588  mbflimsup  25592  mbfmul  25652  itg2cnlem1  25687  ellimc2  25803  dvreslem  25835  dvres2lem  25836  dvidlem  25841  dvmptresicc  25842  dvcnp2  25846  dvcnp2OLD  25847  dvmulbr  25866  dvmulbrOLD  25867  dvcobr  25874  dvcobrOLD  25875  dvrec  25884  dvmptntr  25900  dvcnvlem  25905  lhop1lem  25943  lhop2  25945  itgparts  25979  itgsubstlem  25980  itgpowd  25982  plypf1  26142  taylthlem2  26307  taylthlem2OLD  26308  pserdvlem2  26363  abelth  26376  pige3ALT  26454  efifo  26481  eff1olem  26482  dvlog2  26587  resqrtcn  26684  sqrtcn  26685  dvatan  26870  rlimcnp2  26901  xrlimcnp  26903  efrlim  26904  efrlimOLD  26905  cxp2lim  26912  chpo1ub  27416  dchrisum0lem2a  27453  pnt2  27549  pnt  27550  wlknwwlksnbij  29864  ressnm  32940  gsummpt2d  33024  rmulccn  33936  xrge0mulc1cn  33949  gsumesum  34067  esumsnf  34072  esumcvg  34094  omsmon  34306  carsggect  34326  eulerpartlem1  34375  eulerpartgbij  34380  gsumnunsn  34549  cxpcncf1  34603  itgexpif  34614  reprpmtf1o  34634  elmsubrn  35560  divcnvlin  35765  mptsnunlem  37371  dissneqlem  37373  broucube  37693  mbfposadd  37706  itggt0cn  37729  ftc1anclem3  37734  ftc1anclem8  37739  dvasin  37743  dvacos  37744  areacirc  37752  sdclem2  37781  cncfres  37804  resopunitintvd  42058  resclunitintvd  42059  lcmineqlem2  42062  evlsbagval  42598  pwssplit4  43121  pwfi2f1o  43128  hbtlem6  43161  areaquad  43248  hashnzfzclim  44354  lhe4.4ex1a  44361  resmpti  45214  climresmpt  45696  dvcosre  45949  itgsinexplem1  45991  itgcoscmulx  46006  dirkeritg  46139  dirkercncflem2  46141  fourierdlem16  46160  fourierdlem21  46165  fourierdlem22  46166  fourierdlem57  46200  fourierdlem58  46201  fourierdlem62  46205  fourierdlem83  46226  fourierdlem111  46254  fouriersw  46268  0ome  46566