Theorem resmpt 5996

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114   ⊆ wss 3890  {copab 5148   ↦ cmpt 5167   ↾ cres 5626

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-pr 5370

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-opab 5149  df-mpt 5168  df-xp 5630  df-rel 5631  df-res 5636

This theorem is referenced by:  resmpt3  5997  resmptf  5998  resmptd  5999  mptss  6001  elimampt  6002  fvresex  7906  f1stres  7959  f2ndres  7960  tposss  8170  dftpos2  8186  dftpos4  8188  resixpfo  8877  rlimresb  15518  lo1eq  15521  rlimeq  15522  fsumss  15678  isumclim3  15712  divcnvshft  15811  fprodss  15904  iprodclim3  15956  fprodefsum  16051  bitsf1ocnv  16404  conjsubg  19216  odf1o2  19539  sylow1lem2  19565  sylow2blem1  19586  gsumzres  19875  gsumzsplit  19893  gsumpr  19921  gsumzunsnd  19922  gsum2dlem2  19937  gsummptnn0fz  19952  dprd2da  20010  dpjidcl  20026  ablfac1b  20038  frlmsplit2  21763  psrass1lem  21922  coe1mul2lem2  22243  ofco2  22426  mdetralt  22583  mdetunilem9  22595  tgrest  23134  cmpfi  23383  fmss  23921  txflf  23981  tmdgsum  24070  tgpconncomp  24088  tsmssplit  24127  iscmet3lem3  25267  mbfss  25623  mbfadd  25638  mbfsub  25639  mbflimsup  25643  mbfmul  25703  itg2cnlem1  25738  ellimc2  25854  dvreslem  25886  dvres2lem  25887  dvidlem  25892  dvmptresicc  25893  dvcnp2  25897  dvmulbr  25916  dvcobr  25923  dvrec  25932  dvmptntr  25948  dvcnvlem  25953  lhop1lem  25990  lhop2  25992  itgparts  26024  itgsubstlem  26025  itgpowd  26027  plypf1  26187  taylthlem2  26351  taylthlem2OLD  26352  pserdvlem2  26406  abelth  26419  pige3ALT  26497  efifo  26524  eff1olem  26525  dvlog2  26630  resqrtcn  26726  sqrtcn  26727  dvatan  26912  rlimcnp2  26943  xrlimcnp  26945  efrlim  26946  efrlimOLD  26947  cxp2lim  26954  chpo1ub  27457  dchrisum0lem2a  27494  pnt2  27590  pnt  27591  wlknwwlksnbij  29971  ressnm  33039  gsummpt2d  33125  rmulccn  34088  xrge0mulc1cn  34101  gsumesum  34219  esumsnf  34224  esumcvg  34246  omsmon  34458  carsggect  34478  eulerpartlem1  34527  eulerpartgbij  34532  gsumnunsn  34701  cxpcncf1  34755  itgexpif  34766  reprpmtf1o  34786  elmsubrn  35726  divcnvlin  35931  mptsnunlem  37668  dissneqlem  37670  broucube  37989  mbfposadd  38002  itggt0cn  38025  ftc1anclem3  38030  ftc1anclem8  38035  dvasin  38039  dvacos  38040  areacirc  38048  sdclem2  38077  cncfres  38100  resopunitintvd  42479  resclunitintvd  42480  lcmineqlem2  42483  evlsbagval  43016  pwssplit4  43535  pwfi2f1o  43542  hbtlem6  43575  areaquad  43662  hashnzfzclim  44767  lhe4.4ex1a  44774  resmpti  45626  climresmpt  46105  dvcosre  46358  itgsinexplem1  46400  itgcoscmulx  46415  dirkeritg  46548  dirkercncflem2  46550  fourierdlem16  46569  fourierdlem21  46574  fourierdlem22  46575  fourierdlem57  46609  fourierdlem58  46610  fourierdlem62  46614  fourierdlem83  46635  fourierdlem111  46663  fouriersw  46677  0ome  46975