Theorem resmpt 6057

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1537   ∈ wcel 2106   ⊆ wss 3963  {copab 5210   ↦ cmpt 5231   ↾ cres 5691

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-opab 5211  df-mpt 5232  df-xp 5695  df-rel 5696  df-res 5701

This theorem is referenced by:  resmpt3  6058  resmptf  6059  resmptd  6060  mptss  6062  elimampt  6063  fvresex  7983  f1stres  8037  f2ndres  8038  tposss  8251  dftpos2  8267  dftpos4  8269  resixpfo  8975  rlimresb  15598  lo1eq  15601  rlimeq  15602  fsumss  15758  isumclim3  15792  divcnvshft  15888  fprodss  15981  iprodclim3  16033  fprodefsum  16128  bitsf1ocnv  16478  conjsubg  19281  odf1o2  19606  sylow1lem2  19632  sylow2blem1  19653  gsumzres  19942  gsumzsplit  19960  gsumpr  19988  gsumzunsnd  19989  gsum2dlem2  20004  gsummptnn0fz  20019  dprd2da  20077  dpjidcl  20093  ablfac1b  20105  frlmsplit2  21811  psrass1lem  21970  coe1mul2lem2  22287  ofco2  22473  mdetralt  22630  mdetunilem9  22642  tgrest  23183  cmpfi  23432  fmss  23970  txflf  24030  tmdgsum  24119  tgpconncomp  24137  tsmssplit  24176  iscmet3lem3  25338  mbfss  25695  mbfadd  25710  mbfsub  25711  mbflimsup  25715  mbfmul  25776  itg2cnlem1  25811  ellimc2  25927  dvreslem  25959  dvres2lem  25960  dvidlem  25965  dvmptresicc  25966  dvcnp2  25970  dvcnp2OLD  25971  dvmulbr  25990  dvmulbrOLD  25991  dvcobr  25998  dvcobrOLD  25999  dvrec  26008  dvmptntr  26024  dvcnvlem  26029  lhop1lem  26067  lhop2  26069  itgparts  26103  itgsubstlem  26104  itgpowd  26106  plypf1  26266  taylthlem2  26431  taylthlem2OLD  26432  pserdvlem2  26487  abelth  26500  pige3ALT  26577  efifo  26604  eff1olem  26605  dvlog2  26710  resqrtcn  26807  sqrtcn  26808  dvatan  26993  rlimcnp2  27024  xrlimcnp  27026  efrlim  27027  efrlimOLD  27028  cxp2lim  27035  chpo1ub  27539  dchrisum0lem2a  27576  pnt2  27672  pnt  27673  wlknwwlksnbij  29918  ressnm  32934  gsummpt2d  33035  rmulccn  33889  xrge0mulc1cn  33902  gsumesum  34040  esumsnf  34045  esumcvg  34067  omsmon  34280  carsggect  34300  eulerpartlem1  34349  eulerpartgbij  34354  gsumnunsn  34535  cxpcncf1  34589  itgexpif  34600  reprpmtf1o  34620  elmsubrn  35513  divcnvlin  35713  mptsnunlem  37321  dissneqlem  37323  broucube  37641  mbfposadd  37654  itggt0cn  37677  ftc1anclem3  37682  ftc1anclem8  37687  dvasin  37691  dvacos  37692  areacirc  37700  sdclem2  37729  cncfres  37752  resopunitintvd  42008  resclunitintvd  42009  lcmineqlem2  42012  readvrec  42371  evlsbagval  42553  pwssplit4  43078  pwfi2f1o  43085  hbtlem6  43118  areaquad  43205  hashnzfzclim  44318  lhe4.4ex1a  44325  resmpti  45121  climresmpt  45615  dvcosre  45868  itgsinexplem1  45910  itgcoscmulx  45925  dirkeritg  46058  dirkercncflem2  46060  fourierdlem16  46079  fourierdlem21  46084  fourierdlem22  46085  fourierdlem57  46119  fourierdlem58  46120  fourierdlem62  46124  fourierdlem83  46145  fourierdlem111  46173  fouriersw  46187  0ome  46485