Theorem resmpt 5747

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

Syntax hints:   → wi 4   ∧ wa 387   = wceq 1507   ∈ wcel 2050   ⊆ wss 3823  {copab 4987   ↦ cmpt 5004   ↾ cres 5405

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-ext 2744  ax-sep 5056  ax-nul 5063  ax-pr 5182

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-clab 2753  df-cleq 2765  df-clel 2840  df-nfc 2912  df-rab 3091  df-v 3411  df-dif 3826  df-un 3828  df-in 3830  df-ss 3837  df-nul 4173  df-if 4345  df-sn 4436  df-pr 4438  df-op 4442  df-opab 4988  df-mpt 5005  df-xp 5409  df-rel 5410  df-res 5415

This theorem is referenced by:  resmpt3  5748  resmptf  5749  resmptd  5750  mptss  5752  fvresex  7471  f1stres  7523  f2ndres  7524  tposss  7694  dftpos2  7710  dftpos4  7712  resixpfo  8295  rlimresb  14781  lo1eq  14784  rlimeq  14785  fsumss  14940  isumclim3  14972  divcnvshft  15068  fprodss  15160  iprodclim3  15212  fprodefsum  15306  bitsf1ocnv  15651  conjsubg  18173  psgnunilem5OLD  18396  odf1o2  18471  sylow1lem2  18497  sylow2blem1  18518  gsumzres  18795  gsumzsplit  18812  gsumpr  18840  gsumzunsnd  18841  gsum2dlem2  18856  gsummptnn0fz  18868  dprd2da  18926  dpjidcl  18942  ablfac1b  18954  psrass1lem  19883  coe1mul2lem2  20151  frlmsplit2  20631  ofco2  20776  mdetralt  20933  mdetunilem9  20945  tgrest  21483  cmpfi  21732  cnmptid  21985  fmss  22270  txflf  22330  tmdgsum  22419  tgpconncomp  22436  tsmssplit  22475  iscmet3lem3  23608  mbfss  23962  mbfadd  23977  mbfsub  23978  mbflimsup  23982  mbfmul  24042  itg2cnlem1  24077  ellimc2  24190  dvreslem  24222  dvres2lem  24223  dvidlem  24228  dvcnp2  24232  dvmulbr  24251  dvcobr  24258  dvrec  24267  dvmptntr  24283  dvcnvlem  24288  lhop1lem  24325  lhop2  24327  itgparts  24359  itgsubstlem  24360  tdeglem4  24369  plypf1  24517  taylthlem2  24677  pserdvlem2  24731  abelth  24744  pige3ALT  24820  efifo  24844  eff1olem  24845  dvlog2  24949  resqrtcn  25043  sqrtcn  25044  dvatan  25226  rlimcnp2  25258  xrlimcnp  25260  efrlim  25261  cxp2lim  25268  chpo1ub  25770  dchrisum0lem2a  25807  pnt2  25903  pnt  25904  wlknwwlksnbij  27387  clwlknf1oclwwlknlem3OLD  27622  elimampt  30159  ressnm  30393  gsummpt2d  30553  rmulccn  30844  xrge0mulc1cn  30857  gsumesum  30991  esumsnf  30996  esumcvg  31018  omsmon  31230  carsggect  31250  eulerpartlem1  31299  eulerpartgbij  31304  gsumnunsn  31486  cxpcncf1  31543  itgexpif  31554  reprpmtf1o  31574  elmsubrn  32324  divcnvlin  32513  mptsnunlem  34090  dissneqlem  34092  broucube  34396  mbfposadd  34409  itggt0cn  34434  ftc1anclem3  34439  ftc1anclem8  34444  dvasin  34448  dvacos  34449  areacirc  34457  sdclem2  34488  cncfres  34514  pwssplit4  39114  pwfi2f1o  39121  hbtlem6  39154  itgpowd  39246  areaquad  39248  hashnzfzclim  40099  lhe4.4ex1a  40106  resmpti  40884  climresmpt  41396  dvcosre  41651  dvmptresicc  41659  itgsinexplem1  41694  itgcoscmulx  41709  dirkeritg  41843  dirkercncflem2  41845  fourierdlem16  41864  fourierdlem21  41869  fourierdlem22  41870  fourierdlem57  41904  fourierdlem58  41905  fourierdlem62  41909  fourierdlem83  41930  fourierdlem111  41958  fouriersw  41972  0ome  42267