Theorem resmpt 6023

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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1559   ∈ wcel 2141   ⊆ wss 3904  {copab 5161   ↦ cmpt 5180   ↾ cres 5647

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-12 2211  ax-ext 2733  ax-sep 5245  ax-pr 5389

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3455  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4480  df-sn 4582  df-pr 4584  df-op 4588  df-opab 5162  df-mpt 5181  df-xp 5651  df-rel 5652  df-res 5657

This theorem is referenced by:  resmpt3  6024  resmptf  6025  resmptd  6026  mptss  6028  elimampt  6029  fvresex  7937  f1stres  7990  f2ndres  7991  tposss  8202  dftpos2  8218  dftpos4  8220  resixpfo  8914  rlimresb  15575  lo1eq  15578  rlimeq  15579  fsumss  15735  isumclim3  15769  divcnvshft  15868  fprodss  15961  iprodclim3  16013  fprodefsum  16108  bitsf1ocnv  16461  conjsubg  19273  odf1o2  19596  sylow1lem2  19622  sylow2blem1  19643  gsumzres  19932  gsumzsplit  19950  gsumpr  19978  gsumzunsnd  19979  gsum2dlem2  19994  gsummptnn0fz  20009  dprd2da  20067  dpjidcl  20083  ablfac1b  20095  frlmsplit2  21805  psrass1lem  21965  coe1mul2lem2  22311  ofco2  22491  mdetralt  22648  mdetunilem9  22660  tgrest  23199  cmpfi  23448  fmss  23986  txflf  24046  tmdgsum  24135  tgpconncomp  24153  tsmssplit  24192  iscmet3lem3  25332  mbfss  25688  mbfadd  25703  mbfsub  25704  mbflimsup  25708  mbfmul  25768  itg2cnlem1  25803  ellimc2  25919  dvreslem  25951  dvres2lem  25952  dvidlem  25957  dvmptresicc  25958  dvcnp2  25962  dvmulbr  25981  dvcobr  25988  dvrec  25997  dvmptntr  26013  dvcnvlem  26018  lhop1lem  26055  lhop2  26057  itgparts  26089  itgsubstlem  26090  itgpowd  26092  plypf1  26252  taylthlem2  26414  pserdvlem2  26468  abelth  26481  pige3ALT  26562  efifo  26589  eff1olem  26590  dvlog2  26695  resqrtcn  26791  sqrtcn  26792  dvatan  26977  rlimcnp2  27008  xrlimcnp  27010  efrlim  27011  cxp2lim  27018  chpo1ub  27521  dchrisum0lem2a  27558  pnt2  27654  pnt  27655  wlknwwlksnbij  30034  ressnm  33103  gsummpt2d  33190  rmulccn  34186  xrge0mulc1cn  34199  gsumesum  34317  esumsnf  34322  esumcvg  34344  omsmon  34556  carsggect  34576  eulerpartlem1  34625  eulerpartgbij  34630  gsumnunsn  34799  cxpcncf1  34853  itgexpif  34864  reprpmtf1o  34884  elmsubrn  35842  divcnvlin  36047  mptsnunlem  37796  dissneqlem  37798  broucube  38117  mbfposadd  38130  itggt0cn  38153  ftc1anclem3  38158  ftc1anclem8  38163  dvasin  38167  dvacos  38168  areacirc  38176  sdclem2  38205  cncfres  38228  resopunitintvd  42607  resclunitintvd  42608  lcmineqlem2  42611  evlsbagval  43132  pwssplit4  43630  pwfi2f1o  43637  hbtlem6  43670  areaquad  43757  hashnzfzclim  44862  lhe4.4ex1a  44869  resmpti  45720  climresmpt  46197  dvcosre  46450  itgsinexplem1  46492  itgcoscmulx  46507  dirkeritg  46640  dirkercncflem2  46642  fourierdlem16  46661  fourierdlem21  46666  fourierdlem22  46667  fourierdlem57  46701  fourierdlem58  46702  fourierdlem62  46706  fourierdlem83  46727  fourierdlem111  46755  fouriersw  46769  0ome  47067