Theorem resmpt 5990

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2113   ⊆ wss 3898  {copab 5155   ↦ cmpt 5174   ↾ cres 5621

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-12 2182  ax-ext 2705  ax-sep 5236  ax-nul 5246  ax-pr 5372

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-opab 5156  df-mpt 5175  df-xp 5625  df-rel 5626  df-res 5631

This theorem is referenced by:  resmpt3  5991  resmptf  5992  resmptd  5993  mptss  5995  elimampt  5996  fvresex  7898  f1stres  7951  f2ndres  7952  tposss  8163  dftpos2  8179  dftpos4  8181  resixpfo  8866  rlimresb  15474  lo1eq  15477  rlimeq  15478  fsumss  15634  isumclim3  15668  divcnvshft  15764  fprodss  15857  iprodclim3  15909  fprodefsum  16004  bitsf1ocnv  16357  conjsubg  19164  odf1o2  19487  sylow1lem2  19513  sylow2blem1  19534  gsumzres  19823  gsumzsplit  19841  gsumpr  19869  gsumzunsnd  19870  gsum2dlem2  19885  gsummptnn0fz  19900  dprd2da  19958  dpjidcl  19974  ablfac1b  19986  frlmsplit2  21712  psrass1lem  21871  coe1mul2lem2  22183  ofco2  22367  mdetralt  22524  mdetunilem9  22536  tgrest  23075  cmpfi  23324  fmss  23862  txflf  23922  tmdgsum  24011  tgpconncomp  24029  tsmssplit  24068  iscmet3lem3  25218  mbfss  25575  mbfadd  25590  mbfsub  25591  mbflimsup  25595  mbfmul  25655  itg2cnlem1  25690  ellimc2  25806  dvreslem  25838  dvres2lem  25839  dvidlem  25844  dvmptresicc  25845  dvcnp2  25849  dvcnp2OLD  25850  dvmulbr  25869  dvmulbrOLD  25870  dvcobr  25877  dvcobrOLD  25878  dvrec  25887  dvmptntr  25903  dvcnvlem  25908  lhop1lem  25946  lhop2  25948  itgparts  25982  itgsubstlem  25983  itgpowd  25985  plypf1  26145  taylthlem2  26310  taylthlem2OLD  26311  pserdvlem2  26366  abelth  26379  pige3ALT  26457  efifo  26484  eff1olem  26485  dvlog2  26590  resqrtcn  26687  sqrtcn  26688  dvatan  26873  rlimcnp2  26904  xrlimcnp  26906  efrlim  26907  efrlimOLD  26908  cxp2lim  26915  chpo1ub  27419  dchrisum0lem2a  27456  pnt2  27552  pnt  27553  wlknwwlksnbij  29868  ressnm  32952  gsummpt2d  33036  rmulccn  33962  xrge0mulc1cn  33975  gsumesum  34093  esumsnf  34098  esumcvg  34120  omsmon  34332  carsggect  34352  eulerpartlem1  34401  eulerpartgbij  34406  gsumnunsn  34575  cxpcncf1  34629  itgexpif  34640  reprpmtf1o  34660  elmsubrn  35593  divcnvlin  35798  mptsnunlem  37403  dissneqlem  37405  broucube  37714  mbfposadd  37727  itggt0cn  37750  ftc1anclem3  37755  ftc1anclem8  37760  dvasin  37764  dvacos  37765  areacirc  37773  sdclem2  37802  cncfres  37825  resopunitintvd  42139  resclunitintvd  42140  lcmineqlem2  42143  evlsbagval  42684  pwssplit4  43206  pwfi2f1o  43213  hbtlem6  43246  areaquad  43333  hashnzfzclim  44439  lhe4.4ex1a  44446  resmpti  45299  climresmpt  45781  dvcosre  46034  itgsinexplem1  46076  itgcoscmulx  46091  dirkeritg  46224  dirkercncflem2  46226  fourierdlem16  46245  fourierdlem21  46250  fourierdlem22  46251  fourierdlem57  46285  fourierdlem58  46286  fourierdlem62  46290  fourierdlem83  46311  fourierdlem111  46339  fouriersw  46353  0ome  46651