Theorem resmpt 5449

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

Syntax hints:   → wi 4   ∧ wa 384   = wceq 1483   ∈ wcel 1990   ⊆ wss 3574  {copab 4712   ↦ cmpt 4729   ↾ cres 5116

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-opab 4713  df-mpt 4730  df-xp 5120  df-rel 5121  df-res 5126

This theorem is referenced by:  resmpt3  5450  resmptf  5451  resmptd  5452  mptss  5454  fvresex  7139  f1stres  7190  f2ndres  7191  tposss  7353  dftpos2  7369  dftpos4  7371  resixpfo  7946  rlimresb  14296  lo1eq  14299  rlimeq  14300  fsumss  14456  isumclim3  14490  divcnvshft  14587  fprodss  14678  iprodclim3  14731  fprodefsum  14825  bitsf1ocnv  15166  conjsubg  17692  psgnunilem5  17914  odf1o2  17988  sylow1lem2  18014  sylow2blem1  18035  gsumzres  18310  gsumzsplit  18327  gsumzunsnd  18355  gsum2dlem2  18370  gsummptnn0fz  18382  dprd2da  18441  dpjidcl  18457  ablfac1b  18469  psrass1lem  19377  coe1mul2lem2  19638  frlmsplit2  20112  ofco2  20257  mdetralt  20414  mdetunilem9  20426  tgrest  20963  cmpfi  21211  cnmptid  21464  fmss  21750  txflf  21810  tmdgsum  21899  tgpconncomp  21916  tsmssplit  21955  iscmet3lem3  23088  mbfss  23413  mbfadd  23428  mbfsub  23429  mbflimsup  23433  mbfmul  23493  itg2cnlem1  23528  ellimc2  23641  dvreslem  23673  dvres2lem  23674  dvidlem  23679  dvcnp2  23683  dvmulbr  23702  dvcobr  23709  dvrec  23718  dvmptntr  23734  dvcnvlem  23739  lhop1lem  23776  lhop2  23778  itgparts  23810  itgsubstlem  23811  tdeglem4  23820  plypf1  23968  taylthlem2  24128  pserdvlem2  24182  abelth  24195  pige3  24269  efifo  24293  eff1olem  24294  dvlog2  24399  resqrtcn  24490  sqrtcn  24491  dvatan  24662  rlimcnp2  24693  xrlimcnp  24695  efrlim  24696  cxp2lim  24703  chpo1ub  25169  dchrisum0lem2a  25206  pnt2  25302  pnt  25303  elimampt  29438  ressnm  29651  gsummpt2d  29781  rmulccn  29974  xrge0mulc1cn  29987  gsumesum  30121  esumsnf  30126  esumcvg  30148  omsmon  30360  carsggect  30380  eulerpartlem1  30429  eulerpartgbij  30434  gsumnunsn  30615  cxpcncf1  30673  itgexpif  30684  reprpmtf1o  30704  elmsubrn  31425  divcnvlin  31618  mptsnunlem  33185  dissneqlem  33187  broucube  33443  mbfposadd  33457  itggt0cn  33482  ftc1anclem3  33487  ftc1anclem8  33492  dvasin  33496  dvacos  33497  areacirc  33505  sdclem2  33538  cncfres  33564  pwssplit4  37659  pwfi2f1o  37666  hbtlem6  37699  itgpowd  37800  areaquad  37802  hashnzfzclim  38521  lhe4.4ex1a  38528  resmpti  39359  climresmpt  39891  dvcosre  40126  dvmptresicc  40134  itgsinexplem1  40169  itgcoscmulx  40185  dirkeritg  40319  dirkercncflem2  40321  fourierdlem16  40340  fourierdlem21  40345  fourierdlem22  40346  fourierdlem57  40380  fourierdlem58  40381  fourierdlem62  40385  fourierdlem83  40406  fourierdlem111  40434  fouriersw  40448  0ome  40743  gsumpr  42139