Theorem resmpt 6002

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114   ⊆ wss 3889  {copab 5147   ↦ cmpt 5166   ↾ cres 5633

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-opab 5148  df-mpt 5167  df-xp 5637  df-rel 5638  df-res 5643

This theorem is referenced by:  resmpt3  6003  resmptf  6004  resmptd  6005  mptss  6007  elimampt  6008  fvresex  7913  f1stres  7966  f2ndres  7967  tposss  8177  dftpos2  8193  dftpos4  8195  resixpfo  8884  rlimresb  15527  lo1eq  15530  rlimeq  15531  fsumss  15687  isumclim3  15721  divcnvshft  15820  fprodss  15913  iprodclim3  15965  fprodefsum  16060  bitsf1ocnv  16413  conjsubg  19225  odf1o2  19548  sylow1lem2  19574  sylow2blem1  19595  gsumzres  19884  gsumzsplit  19902  gsumpr  19930  gsumzunsnd  19931  gsum2dlem2  19946  gsummptnn0fz  19961  dprd2da  20019  dpjidcl  20035  ablfac1b  20047  frlmsplit2  21753  psrass1lem  21912  coe1mul2lem2  22233  ofco2  22416  mdetralt  22573  mdetunilem9  22585  tgrest  23124  cmpfi  23373  fmss  23911  txflf  23971  tmdgsum  24060  tgpconncomp  24078  tsmssplit  24117  iscmet3lem3  25257  mbfss  25613  mbfadd  25628  mbfsub  25629  mbflimsup  25633  mbfmul  25693  itg2cnlem1  25728  ellimc2  25844  dvreslem  25876  dvres2lem  25877  dvidlem  25882  dvmptresicc  25883  dvcnp2  25887  dvmulbr  25906  dvcobr  25913  dvrec  25922  dvmptntr  25938  dvcnvlem  25943  lhop1lem  25980  lhop2  25982  itgparts  26014  itgsubstlem  26015  itgpowd  26017  plypf1  26177  taylthlem2  26339  pserdvlem2  26393  abelth  26406  pige3ALT  26484  efifo  26511  eff1olem  26512  dvlog2  26617  resqrtcn  26713  sqrtcn  26714  dvatan  26899  rlimcnp2  26930  xrlimcnp  26932  efrlim  26933  cxp2lim  26940  chpo1ub  27443  dchrisum0lem2a  27480  pnt2  27576  pnt  27577  wlknwwlksnbij  29956  ressnm  33024  gsummpt2d  33110  rmulccn  34072  xrge0mulc1cn  34085  gsumesum  34203  esumsnf  34208  esumcvg  34230  omsmon  34442  carsggect  34462  eulerpartlem1  34511  eulerpartgbij  34516  gsumnunsn  34685  cxpcncf1  34739  itgexpif  34750  reprpmtf1o  34770  elmsubrn  35710  divcnvlin  35915  mptsnunlem  37654  dissneqlem  37656  broucube  37975  mbfposadd  37988  itggt0cn  38011  ftc1anclem3  38016  ftc1anclem8  38021  dvasin  38025  dvacos  38026  areacirc  38034  sdclem2  38063  cncfres  38086  resopunitintvd  42465  resclunitintvd  42466  lcmineqlem2  42469  evlsbagval  43002  pwssplit4  43517  pwfi2f1o  43524  hbtlem6  43557  areaquad  43644  hashnzfzclim  44749  lhe4.4ex1a  44756  resmpti  45608  climresmpt  46087  dvcosre  46340  itgsinexplem1  46382  itgcoscmulx  46397  dirkeritg  46530  dirkercncflem2  46532  fourierdlem16  46551  fourierdlem21  46556  fourierdlem22  46557  fourierdlem57  46591  fourierdlem58  46592  fourierdlem62  46596  fourierdlem83  46617  fourierdlem111  46645  fouriersw  46659  0ome  46957