Theorem resmpt 5981

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

Syntax hints:   → wi 4   ∧ wa 397   = wceq 1541   ∈ wcel 2106   ⊆ wss 3901  {copab 5158   ↦ cmpt 5179   ↾ 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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-12 2171  ax-ext 2708  ax-sep 5247  ax-nul 5254  ax-pr 5376

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-clab 2715  df-cleq 2729  df-clel 2815  df-rab 3405  df-v 3444  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4274  df-if 4478  df-sn 4578  df-pr 4580  df-op 4584  df-opab 5159  df-mpt 5180  df-xp 5630  df-rel 5631  df-res 5636

This theorem is referenced by:  resmpt3  5982  resmptf  5983  resmptd  5984  mptss  5986  fvresex  7874  f1stres  7927  f2ndres  7928  tposss  8117  dftpos2  8133  dftpos4  8135  resixpfo  8799  rlimresb  15373  lo1eq  15376  rlimeq  15377  fsumss  15536  isumclim3  15570  divcnvshft  15666  fprodss  15757  iprodclim3  15809  fprodefsum  15903  bitsf1ocnv  16250  conjsubg  18962  odf1o2  19274  sylow1lem2  19300  sylow2blem1  19321  gsumzres  19604  gsumzsplit  19622  gsumpr  19650  gsumzunsnd  19651  gsum2dlem2  19666  gsummptnn0fz  19681  dprd2da  19739  dpjidcl  19755  ablfac1b  19767  frlmsplit2  21085  psrass1lemOLD  21248  psrass1lem  21251  coe1mul2lem2  21544  ofco2  21705  mdetralt  21862  mdetunilem9  21874  tgrest  22415  cmpfi  22664  fmss  23202  txflf  23262  tmdgsum  23351  tgpconncomp  23369  tsmssplit  23408  iscmet3lem3  24559  mbfss  24915  mbfadd  24930  mbfsub  24931  mbflimsup  24935  mbfmul  24996  itg2cnlem1  25031  ellimc2  25146  dvreslem  25178  dvres2lem  25179  dvidlem  25184  dvmptresicc  25185  dvcnp2  25189  dvmulbr  25208  dvcobr  25215  dvrec  25224  dvmptntr  25240  dvcnvlem  25245  lhop1lem  25282  lhop2  25284  itgparts  25316  itgsubstlem  25317  itgpowd  25319  tdeglem4OLD  25330  plypf1  25478  taylthlem2  25638  pserdvlem2  25692  abelth  25705  pige3ALT  25781  efifo  25808  eff1olem  25809  dvlog2  25913  resqrtcn  26007  sqrtcn  26008  dvatan  26190  rlimcnp2  26221  xrlimcnp  26223  efrlim  26224  cxp2lim  26231  chpo1ub  26733  dchrisum0lem2a  26770  pnt2  26866  pnt  26867  wlknwwlksnbij  28540  elimampt  31258  ressnm  31521  gsummpt2d  31594  rmulccn  32174  xrge0mulc1cn  32187  gsumesum  32323  esumsnf  32328  esumcvg  32350  omsmon  32563  carsggect  32583  eulerpartlem1  32632  eulerpartgbij  32637  gsumnunsn  32818  cxpcncf1  32873  itgexpif  32884  reprpmtf1o  32904  elmsubrn  33787  divcnvlin  33988  mptsnunlem  35663  dissneqlem  35665  broucube  35967  mbfposadd  35980  itggt0cn  36003  ftc1anclem3  36008  ftc1anclem8  36013  dvasin  36017  dvacos  36018  areacirc  36026  sdclem2  36056  cncfres  36079  resopunitintvd  40339  resclunitintvd  40340  lcmineqlem2  40343  pwssplit4  41228  pwfi2f1o  41235  hbtlem6  41268  areaquad  41362  hashnzfzclim  42313  lhe4.4ex1a  42320  resmpti  43093  climresmpt  43588  dvcosre  43841  itgsinexplem1  43883  itgcoscmulx  43898  dirkeritg  44031  dirkercncflem2  44033  fourierdlem16  44052  fourierdlem21  44057  fourierdlem22  44058  fourierdlem57  44092  fourierdlem58  44093  fourierdlem62  44097  fourierdlem83  44118  fourierdlem111  44146  fouriersw  44160  0ome  44456