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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1547   ∈ wcel 2119   ⊆ wss 3890  {copab 5141   ↦ cmpt 5160   ↾ cres 5627

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-12 2189  ax-ext 2712  ax-sep 5225  ax-pr 5369

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-opab 5142  df-mpt 5161  df-xp 5631  df-rel 5632  df-res 5637

This theorem is referenced by:  resmpt3  5997  resmptf  5998  resmptd  5999  mptss  6001  elimampt  6002  fvresex  7909  f1stres  7962  f2ndres  7963  tposss  8174  dftpos2  8190  dftpos4  8192  resixpfo  8881  rlimresb  15525  lo1eq  15528  rlimeq  15529  fsumss  15685  isumclim3  15719  divcnvshft  15818  fprodss  15911  iprodclim3  15963  fprodefsum  16058  bitsf1ocnv  16411  conjsubg  19223  odf1o2  19546  sylow1lem2  19572  sylow2blem1  19593  gsumzres  19882  gsumzsplit  19900  gsumpr  19928  gsumzunsnd  19929  gsum2dlem2  19944  gsummptnn0fz  19959  dprd2da  20017  dpjidcl  20033  ablfac1b  20045  frlmsplit2  21755  psrass1lem  21915  coe1mul2lem2  22261  ofco2  22441  mdetralt  22598  mdetunilem9  22610  tgrest  23149  cmpfi  23398  fmss  23936  txflf  23996  tmdgsum  24085  tgpconncomp  24103  tsmssplit  24142  iscmet3lem3  25282  mbfss  25638  mbfadd  25653  mbfsub  25654  mbflimsup  25658  mbfmul  25718  itg2cnlem1  25753  ellimc2  25869  dvreslem  25901  dvres2lem  25902  dvidlem  25907  dvmptresicc  25908  dvcnp2  25912  dvmulbr  25931  dvcobr  25938  dvrec  25947  dvmptntr  25963  dvcnvlem  25968  lhop1lem  26005  lhop2  26007  itgparts  26039  itgsubstlem  26040  itgpowd  26042  plypf1  26202  taylthlem2  26364  pserdvlem2  26418  abelth  26431  pige3ALT  26509  efifo  26536  eff1olem  26537  dvlog2  26642  resqrtcn  26738  sqrtcn  26739  dvatan  26924  rlimcnp2  26955  xrlimcnp  26957  efrlim  26958  cxp2lim  26965  chpo1ub  27468  dchrisum0lem2a  27505  pnt2  27601  pnt  27602  wlknwwlksnbij  29981  ressnm  33050  gsummpt2d  33137  rmulccn  34119  xrge0mulc1cn  34132  gsumesum  34250  esumsnf  34255  esumcvg  34277  omsmon  34489  carsggect  34509  eulerpartlem1  34558  eulerpartgbij  34563  gsumnunsn  34732  cxpcncf1  34786  itgexpif  34797  reprpmtf1o  34817  elmsubrn  35763  divcnvlin  35968  mptsnunlem  37707  dissneqlem  37709  broucube  38028  mbfposadd  38041  itggt0cn  38064  ftc1anclem3  38069  ftc1anclem8  38074  dvasin  38078  dvacos  38079  areacirc  38087  sdclem2  38116  cncfres  38139  resopunitintvd  42518  resclunitintvd  42519  lcmineqlem2  42522  evlsbagval  43043  pwssplit4  43541  pwfi2f1o  43548  hbtlem6  43581  areaquad  43668  hashnzfzclim  44773  lhe4.4ex1a  44780  resmpti  45632  climresmpt  46109  dvcosre  46362  itgsinexplem1  46404  itgcoscmulx  46419  dirkeritg  46552  dirkercncflem2  46554  fourierdlem16  46573  fourierdlem21  46578  fourierdlem22  46579  fourierdlem57  46613  fourierdlem58  46614  fourierdlem62  46618  fourierdlem83  46639  fourierdlem111  46667  fouriersw  46681  0ome  46979