Theorem resmpt 6046

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

Syntax hints:   → wi 4   ∧ wa 394   = wceq 1534   ∈ wcel 2099   ⊆ wss 3947  {copab 5215   ↦ cmpt 5236   ↾ cres 5684

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-12 2167  ax-ext 2697  ax-sep 5304  ax-nul 5311  ax-pr 5433

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-rab 3420  df-v 3464  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4326  df-if 4534  df-sn 4634  df-pr 4636  df-op 4640  df-opab 5216  df-mpt 5237  df-xp 5688  df-rel 5689  df-res 5694

This theorem is referenced by:  resmpt3  6047  resmptf  6048  resmptd  6049  mptss  6051  elimampt  6052  fvresex  7973  f1stres  8027  f2ndres  8028  tposss  8242  dftpos2  8258  dftpos4  8260  resixpfo  8965  rlimresb  15567  lo1eq  15570  rlimeq  15571  fsumss  15729  isumclim3  15763  divcnvshft  15859  fprodss  15950  iprodclim3  16002  fprodefsum  16097  bitsf1ocnv  16444  conjsubg  19244  odf1o2  19571  sylow1lem2  19597  sylow2blem1  19618  gsumzres  19907  gsumzsplit  19925  gsumpr  19953  gsumzunsnd  19954  gsum2dlem2  19969  gsummptnn0fz  19984  dprd2da  20042  dpjidcl  20058  ablfac1b  20070  frlmsplit2  21771  psrass1lemOLD  21938  psrass1lem  21941  coe1mul2lem2  22259  ofco2  22444  mdetralt  22601  mdetunilem9  22613  tgrest  23154  cmpfi  23403  fmss  23941  txflf  24001  tmdgsum  24090  tgpconncomp  24108  tsmssplit  24147  iscmet3lem3  25309  mbfss  25666  mbfadd  25681  mbfsub  25682  mbflimsup  25686  mbfmul  25747  itg2cnlem1  25782  ellimc2  25897  dvreslem  25929  dvres2lem  25930  dvidlem  25935  dvmptresicc  25936  dvcnp2  25940  dvcnp2OLD  25941  dvmulbr  25960  dvmulbrOLD  25961  dvcobr  25968  dvcobrOLD  25969  dvrec  25978  dvmptntr  25994  dvcnvlem  25999  lhop1lem  26037  lhop2  26039  itgparts  26073  itgsubstlem  26074  itgpowd  26076  tdeglem4OLD  26087  plypf1  26239  taylthlem2  26402  taylthlem2OLD  26403  pserdvlem2  26458  abelth  26471  pige3ALT  26547  efifo  26574  eff1olem  26575  dvlog2  26680  resqrtcn  26777  sqrtcn  26778  dvatan  26963  rlimcnp2  26994  xrlimcnp  26996  efrlim  26997  efrlimOLD  26998  cxp2lim  27005  chpo1ub  27509  dchrisum0lem2a  27546  pnt2  27642  pnt  27643  wlknwwlksnbij  29822  ressnm  32828  gsummpt2d  32917  rmulccn  33743  xrge0mulc1cn  33756  gsumesum  33892  esumsnf  33897  esumcvg  33919  omsmon  34132  carsggect  34152  eulerpartlem1  34201  eulerpartgbij  34206  gsumnunsn  34387  cxpcncf1  34441  itgexpif  34452  reprpmtf1o  34472  elmsubrn  35356  divcnvlin  35555  mptsnunlem  37045  dissneqlem  37047  broucube  37355  mbfposadd  37368  itggt0cn  37391  ftc1anclem3  37396  ftc1anclem8  37401  dvasin  37405  dvacos  37406  areacirc  37414  sdclem2  37443  cncfres  37466  resopunitintvd  41725  resclunitintvd  41726  lcmineqlem2  41729  evlsbagval  42038  pwssplit4  42750  pwfi2f1o  42757  hbtlem6  42790  areaquad  42881  hashnzfzclim  43996  lhe4.4ex1a  44003  resmpti  44785  climresmpt  45280  dvcosre  45533  itgsinexplem1  45575  itgcoscmulx  45590  dirkeritg  45723  dirkercncflem2  45725  fourierdlem16  45744  fourierdlem21  45749  fourierdlem22  45750  fourierdlem57  45784  fourierdlem58  45785  fourierdlem62  45789  fourierdlem83  45810  fourierdlem111  45838  fouriersw  45852  0ome  46150