Theorem resmpt 6008

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109   ⊆ wss 3914  {copab 5169   ↦ cmpt 5188   ↾ cres 5640

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-opab 5170  df-mpt 5189  df-xp 5644  df-rel 5645  df-res 5650

This theorem is referenced by:  resmpt3  6009  resmptf  6010  resmptd  6011  mptss  6013  elimampt  6014  fvresex  7938  f1stres  7992  f2ndres  7993  tposss  8206  dftpos2  8222  dftpos4  8224  resixpfo  8909  rlimresb  15531  lo1eq  15534  rlimeq  15535  fsumss  15691  isumclim3  15725  divcnvshft  15821  fprodss  15914  iprodclim3  15966  fprodefsum  16061  bitsf1ocnv  16414  conjsubg  19182  odf1o2  19503  sylow1lem2  19529  sylow2blem1  19550  gsumzres  19839  gsumzsplit  19857  gsumpr  19885  gsumzunsnd  19886  gsum2dlem2  19901  gsummptnn0fz  19916  dprd2da  19974  dpjidcl  19990  ablfac1b  20002  frlmsplit2  21682  psrass1lem  21841  coe1mul2lem2  22154  ofco2  22338  mdetralt  22495  mdetunilem9  22507  tgrest  23046  cmpfi  23295  fmss  23833  txflf  23893  tmdgsum  23982  tgpconncomp  24000  tsmssplit  24039  iscmet3lem3  25190  mbfss  25547  mbfadd  25562  mbfsub  25563  mbflimsup  25567  mbfmul  25627  itg2cnlem1  25662  ellimc2  25778  dvreslem  25810  dvres2lem  25811  dvidlem  25816  dvmptresicc  25817  dvcnp2  25821  dvcnp2OLD  25822  dvmulbr  25841  dvmulbrOLD  25842  dvcobr  25849  dvcobrOLD  25850  dvrec  25859  dvmptntr  25875  dvcnvlem  25880  lhop1lem  25918  lhop2  25920  itgparts  25954  itgsubstlem  25955  itgpowd  25957  plypf1  26117  taylthlem2  26282  taylthlem2OLD  26283  pserdvlem2  26338  abelth  26351  pige3ALT  26429  efifo  26456  eff1olem  26457  dvlog2  26562  resqrtcn  26659  sqrtcn  26660  dvatan  26845  rlimcnp2  26876  xrlimcnp  26878  efrlim  26879  efrlimOLD  26880  cxp2lim  26887  chpo1ub  27391  dchrisum0lem2a  27428  pnt2  27524  pnt  27525  wlknwwlksnbij  29818  ressnm  32886  gsummpt2d  32989  rmulccn  33918  xrge0mulc1cn  33931  gsumesum  34049  esumsnf  34054  esumcvg  34076  omsmon  34289  carsggect  34309  eulerpartlem1  34358  eulerpartgbij  34363  gsumnunsn  34532  cxpcncf1  34586  itgexpif  34597  reprpmtf1o  34617  elmsubrn  35515  divcnvlin  35720  mptsnunlem  37326  dissneqlem  37328  broucube  37648  mbfposadd  37661  itggt0cn  37684  ftc1anclem3  37689  ftc1anclem8  37694  dvasin  37698  dvacos  37699  areacirc  37707  sdclem2  37736  cncfres  37759  resopunitintvd  42014  resclunitintvd  42015  lcmineqlem2  42018  evlsbagval  42554  pwssplit4  43078  pwfi2f1o  43085  hbtlem6  43118  areaquad  43205  hashnzfzclim  44311  lhe4.4ex1a  44318  resmpti  45172  climresmpt  45657  dvcosre  45910  itgsinexplem1  45952  itgcoscmulx  45967  dirkeritg  46100  dirkercncflem2  46102  fourierdlem16  46121  fourierdlem21  46126  fourierdlem22  46127  fourierdlem57  46161  fourierdlem58  46162  fourierdlem62  46166  fourierdlem83  46187  fourierdlem111  46215  fouriersw  46229  0ome  46527