Theorem resmpt 6031

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2145   ⊆ wss 3899  {copab 5167   ↦ cmpt 5186   ↾ cres 5653

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-opab 5168  df-mpt 5187  df-xp 5657  df-rel 5658  df-res 5663

This theorem is used by:  resmpt3  6032  resmptf  6033  resmptd  6034  mptss  6036  elimampt  6037  fvresex  7961  f1stres  8014  f2ndres  8015  tposss  8228  dftpos2  8244  dftpos4  8246  resixpfo  8948  rlimresb  15712  lo1eq  15715  rlimeq  15716  fsumss  15871  isumclim3  15905  divcnvshft  16004  fprodss  16095  iprodclim3  16147  fprodefsum  16241  bitsf1ocnv  16594  conjsubg  19444  odf1o2  19767  sylow1lem2  19793  sylow2blem1  19814  gsumzres  20103  gsumzsplit  20121  gsumpr  20149  gsumzunsnd  20150  gsum2dlem2  20165  gsummptnn0fz  20180  dprd2da  20238  dpjidcl  20254  ablfac1b  20266  frlmsplit2  22059  psrass1lem  22221  coe1mul2lem2  22567  ofco2  22746  mdetralt  22903  mdetunilem9  22915  tgrest  23457  cmpfi  23706  fmss  24245  txflf  24305  tmdgsum  24394  tgpconncomp  24412  tsmssplit  24451  iscmet3lem3  25591  mbfss  25947  mbfadd  25962  mbfsub  25963  mbflimsup  25967  mbfmul  26027  itg2cnlem1  26062  ellimc2  26177  dvreslem  26209  dvres2lem  26210  dvidlem  26215  dvmptresicc  26216  dvcnp2  26220  dvmulbr  26239  dvcobr  26246  dvrec  26255  dvmptntr  26271  dvcnvlem  26276  lhop1lem  26313  lhop2  26315  itgparts  26347  itgsubstlem  26348  itgpowd  26350  plypf1  26511  taylthlem2  26683  pserdvlem2  26737  abelth  26750  pige3ALT  26830  efifo  26857  eff1olem  26858  dvlog2  26963  resqrtcn  27059  sqrtcn  27060  dvatan  27245  rlimcnp2  27276  xrlimcnp  27278  efrlim  27279  cxp2lim  27286  chpo1ub  27789  dchrisum0lem2a  27826  pnt2  27922  pnt  27923  wlknwwlksnbij  30459  ressnm  33507  gsummpt2d  33592  rmulccn  34542  xrge0mulc1cn  34555  gsumesum  34673  esumsnf  34678  esumcvg  34700  omsmon  34913  carsggect  34933  eulerpartlem1  34982  eulerpartgbij  34987  gsumnunsn  35156  cxpcncf1  35207  itgexpif  35218  reprpmtf1o  35238  elmsubrn  36262  divcnvlin  36467  mptsnunlem  38229  dissneqlem  38231  broucube  38540  mbfposadd  38553  itggt0cn  38576  ftc1anclem3  38581  ftc1anclem8  38586  dvasin  38590  dvacos  38591  areacirc  38599  sdclem2  38644  cncfres  38667  resopunitintvd  43044  resclunitintvd  43045  lcmineqlem2  43048  evlsbagval  43576  pwssplit4  44049  pwfi2f1o  44056  hbtlem6  44089  areaquad  44176  hashnzfzclim  45265  lhe4.4ex1a  45272  resmpti  46136  climresmpt  46613  dvcosre  46866  itgsinexplem1  46908  itgcoscmulx  46923  dirkeritg  47056  dirkercncflem2  47058  fourierdlem16  47077  fourierdlem21  47082  fourierdlem22  47083  fourierdlem57  47117  fourierdlem58  47118  fourierdlem62  47122  fourierdlem83  47143  fourierdlem111  47171  fouriersw  47185  0ome  47483