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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2113   ⊆ wss 3901  {copab 5160   ↦ cmpt 5179   ↾ cres 5626

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-opab 5161  df-mpt 5180  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  7904  f1stres  7957  f2ndres  7958  tposss  8169  dftpos2  8185  dftpos4  8187  resixpfo  8874  rlimresb  15488  lo1eq  15491  rlimeq  15492  fsumss  15648  isumclim3  15682  divcnvshft  15778  fprodss  15871  iprodclim3  15923  fprodefsum  16018  bitsf1ocnv  16371  conjsubg  19179  odf1o2  19502  sylow1lem2  19528  sylow2blem1  19549  gsumzres  19838  gsumzsplit  19856  gsumpr  19884  gsumzunsnd  19885  gsum2dlem2  19900  gsummptnn0fz  19915  dprd2da  19973  dpjidcl  19989  ablfac1b  20001  frlmsplit2  21728  psrass1lem  21888  coe1mul2lem2  22210  ofco2  22395  mdetralt  22552  mdetunilem9  22564  tgrest  23103  cmpfi  23352  fmss  23890  txflf  23950  tmdgsum  24039  tgpconncomp  24057  tsmssplit  24096  iscmet3lem3  25246  mbfss  25603  mbfadd  25618  mbfsub  25619  mbflimsup  25623  mbfmul  25683  itg2cnlem1  25718  ellimc2  25834  dvreslem  25866  dvres2lem  25867  dvidlem  25872  dvmptresicc  25873  dvcnp2  25877  dvcnp2OLD  25878  dvmulbr  25897  dvmulbrOLD  25898  dvcobr  25905  dvcobrOLD  25906  dvrec  25915  dvmptntr  25931  dvcnvlem  25936  lhop1lem  25974  lhop2  25976  itgparts  26010  itgsubstlem  26011  itgpowd  26013  plypf1  26173  taylthlem2  26338  taylthlem2OLD  26339  pserdvlem2  26394  abelth  26407  pige3ALT  26485  efifo  26512  eff1olem  26513  dvlog2  26618  resqrtcn  26715  sqrtcn  26716  dvatan  26901  rlimcnp2  26932  xrlimcnp  26934  efrlim  26935  efrlimOLD  26936  cxp2lim  26943  chpo1ub  27447  dchrisum0lem2a  27484  pnt2  27580  pnt  27581  wlknwwlksnbij  29961  ressnm  33046  gsummpt2d  33132  rmulccn  34085  xrge0mulc1cn  34098  gsumesum  34216  esumsnf  34221  esumcvg  34243  omsmon  34455  carsggect  34475  eulerpartlem1  34524  eulerpartgbij  34529  gsumnunsn  34698  cxpcncf1  34752  itgexpif  34763  reprpmtf1o  34783  elmsubrn  35722  divcnvlin  35927  mptsnunlem  37539  dissneqlem  37541  broucube  37851  mbfposadd  37864  itggt0cn  37887  ftc1anclem3  37892  ftc1anclem8  37897  dvasin  37901  dvacos  37902  areacirc  37910  sdclem2  37939  cncfres  37962  resopunitintvd  42276  resclunitintvd  42277  lcmineqlem2  42280  evlsbagval  42808  pwssplit4  43327  pwfi2f1o  43334  hbtlem6  43367  areaquad  43454  hashnzfzclim  44559  lhe4.4ex1a  44566  resmpti  45418  climresmpt  45899  dvcosre  46152  itgsinexplem1  46194  itgcoscmulx  46209  dirkeritg  46342  dirkercncflem2  46344  fourierdlem16  46363  fourierdlem21  46368  fourierdlem22  46369  fourierdlem57  46403  fourierdlem58  46404  fourierdlem62  46408  fourierdlem83  46429  fourierdlem111  46457  fouriersw  46471  0ome  46769