Theorem resmpt 5934

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1539   ∈ wcel 2108   ⊆ wss 3883  {copab 5132   ↦ cmpt 5153   ↾ cres 5582

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-opab 5133  df-mpt 5154  df-xp 5586  df-rel 5587  df-res 5592

This theorem is referenced by:  resmpt3  5935  resmptf  5936  resmptd  5937  mptss  5939  fvresex  7776  f1stres  7828  f2ndres  7829  tposss  8014  dftpos2  8030  dftpos4  8032  resixpfo  8682  rlimresb  15202  lo1eq  15205  rlimeq  15206  fsumss  15365  isumclim3  15399  divcnvshft  15495  fprodss  15586  iprodclim3  15638  fprodefsum  15732  bitsf1ocnv  16079  conjsubg  18781  odf1o2  19093  sylow1lem2  19119  sylow2blem1  19140  gsumzres  19425  gsumzsplit  19443  gsumpr  19471  gsumzunsnd  19472  gsum2dlem2  19487  gsummptnn0fz  19502  dprd2da  19560  dpjidcl  19576  ablfac1b  19588  frlmsplit2  20890  psrass1lemOLD  21053  psrass1lem  21056  coe1mul2lem2  21349  ofco2  21508  mdetralt  21665  mdetunilem9  21677  tgrest  22218  cmpfi  22467  fmss  23005  txflf  23065  tmdgsum  23154  tgpconncomp  23172  tsmssplit  23211  iscmet3lem3  24359  mbfss  24715  mbfadd  24730  mbfsub  24731  mbflimsup  24735  mbfmul  24796  itg2cnlem1  24831  ellimc2  24946  dvreslem  24978  dvres2lem  24979  dvidlem  24984  dvmptresicc  24985  dvcnp2  24989  dvmulbr  25008  dvcobr  25015  dvrec  25024  dvmptntr  25040  dvcnvlem  25045  lhop1lem  25082  lhop2  25084  itgparts  25116  itgsubstlem  25117  itgpowd  25119  tdeglem4OLD  25130  plypf1  25278  taylthlem2  25438  pserdvlem2  25492  abelth  25505  pige3ALT  25581  efifo  25608  eff1olem  25609  dvlog2  25713  resqrtcn  25807  sqrtcn  25808  dvatan  25990  rlimcnp2  26021  xrlimcnp  26023  efrlim  26024  cxp2lim  26031  chpo1ub  26533  dchrisum0lem2a  26570  pnt2  26666  pnt  26667  wlknwwlksnbij  28154  elimampt  30874  ressnm  31138  gsummpt2d  31211  rmulccn  31780  xrge0mulc1cn  31793  gsumesum  31927  esumsnf  31932  esumcvg  31954  omsmon  32165  carsggect  32185  eulerpartlem1  32234  eulerpartgbij  32239  gsumnunsn  32420  cxpcncf1  32475  itgexpif  32486  reprpmtf1o  32506  elmsubrn  33390  divcnvlin  33604  mptsnunlem  35436  dissneqlem  35438  broucube  35738  mbfposadd  35751  itggt0cn  35774  ftc1anclem3  35779  ftc1anclem8  35784  dvasin  35788  dvacos  35789  areacirc  35797  sdclem2  35827  cncfres  35850  resopunitintvd  39962  resclunitintvd  39963  lcmineqlem2  39966  pwssplit4  40830  pwfi2f1o  40837  hbtlem6  40870  areaquad  40963  hashnzfzclim  41829  lhe4.4ex1a  41836  resmpti  42603  climresmpt  43090  dvcosre  43343  itgsinexplem1  43385  itgcoscmulx  43400  dirkeritg  43533  dirkercncflem2  43535  fourierdlem16  43554  fourierdlem21  43559  fourierdlem22  43560  fourierdlem57  43594  fourierdlem58  43595  fourierdlem62  43599  fourierdlem83  43620  fourierdlem111  43648  fouriersw  43662  0ome  43957