Theorem resmpt 6028

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1569   ∈ wcel 2144   ⊆ wss 3895  {copab 5166   ↦ cmpt 5185   ↾ cres 5652

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-opab 5167  df-mpt 5186  df-xp 5656  df-rel 5657  df-res 5662

This theorem is used by:  resmpt3  6029  resmptf  6030  resmptd  6031  mptss  6033  elimampt  6034  fvresex  7972  f1stres  8025  f2ndres  8026  tposss  8247  dftpos2  8263  dftpos4  8265  resixpfo  8967  rlimresb  15737  lo1eq  15740  rlimeq  15741  fsumss  15896  isumclim3  15930  divcnvshft  16029  fprodss  16120  iprodclim3  16172  fprodefsum  16266  bitsf1ocnv  16619  conjsubg  19469  odf1o2  19792  sylow1lem2  19818  sylow2blem1  19839  gsumzres  20128  gsumzsplit  20146  gsumpr  20174  gsumzunsnd  20175  gsum2dlem2  20190  gsummptnn0fz  20205  dprd2da  20263  dpjidcl  20279  ablfac1b  20291  frlmsplit2  22084  psrass1lem  22246  coe1mul2lem2  22592  ofco2  22771  mdetralt  22928  mdetunilem9  22940  tgrest  23482  cmpfi  23731  fmss  24270  txflf  24330  tmdgsum  24419  tgpconncomp  24437  tsmssplit  24476  iscmet3lem3  25616  mbfss  25972  mbfadd  25987  mbfsub  25988  mbflimsup  25992  mbfmul  26052  itg2cnlem1  26087  ellimc2  26202  dvreslem  26234  dvres2lem  26235  dvidlem  26240  dvmptresicc  26241  dvcnp2  26245  dvmulbr  26264  dvcobr  26271  dvrec  26280  dvmptntr  26296  dvcnvlem  26301  lhop1lem  26338  lhop2  26340  itgparts  26372  itgsubstlem  26373  itgpowd  26375  plypf1  26536  taylthlem2  26706  pserdvlem2  26760  abelth  26773  pige3ALT  26853  efifo  26880  eff1olem  26881  dvlog2  26986  resqrtcn  27082  sqrtcn  27083  dvatan  27268  rlimcnp2  27299  xrlimcnp  27301  efrlim  27302  cxp2lim  27309  chpo1ub  27812  dchrisum0lem2a  27849  pnt2  27945  pnt  27946  wlknwwlksnbij  30482  ressnm  33571  gsummpt2d  33656  rmulccn  34606  xrge0mulc1cn  34619  gsumesum  34737  esumsnf  34742  esumcvg  34764  omsmon  34976  carsggect  34996  eulerpartlem1  35045  eulerpartgbij  35050  gsumnunsn  35219  cxpcncf1  35270  itgexpif  35281  reprpmtf1o  35301  elmsubrn  36379  divcnvlin  36590  mptsnunlem  38354  dissneqlem  38356  broucube  38665  mbfposadd  38678  itggt0cn  38701  ftc1anclem3  38706  ftc1anclem8  38711  dvasin  38715  dvacos  38716  areacirc  38724  sdclem2  38769  cncfres  38792  resopunitintvd  43169  resclunitintvd  43170  lcmineqlem2  43173  evlsbagval  43707  pwssplit4  44184  pwfi2f1o  44191  hbtlem6  44224  areaquad  44311  hashnzfzclim  45399  lhe4.4ex1a  45406  resmpti  46286  climresmpt  46762  dvcosre  47015  itgsinexplem1  47057  itgcoscmulx  47072  dirkeritg  47205  dirkercncflem2  47207  fourierdlem16  47226  fourierdlem21  47231  fourierdlem22  47232  fourierdlem57  47266  fourierdlem58  47267  fourierdlem62  47271  fourierdlem83  47292  fourierdlem111  47320  fouriersw  47334  0ome  47632