Theorem resmpt 5992

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109   ⊆ wss 3905  {copab 5157   ↦ cmpt 5176   ↾ cres 5625

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-12 2178  ax-ext 2701  ax-sep 5238  ax-nul 5248  ax-pr 5374

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-opab 5158  df-mpt 5177  df-xp 5629  df-rel 5630  df-res 5635

This theorem is referenced by:  resmpt3  5993  resmptf  5994  resmptd  5995  mptss  5997  elimampt  5998  fvresex  7902  f1stres  7955  f2ndres  7956  tposss  8167  dftpos2  8183  dftpos4  8185  resixpfo  8870  rlimresb  15490  lo1eq  15493  rlimeq  15494  fsumss  15650  isumclim3  15684  divcnvshft  15780  fprodss  15873  iprodclim3  15925  fprodefsum  16020  bitsf1ocnv  16373  conjsubg  19147  odf1o2  19470  sylow1lem2  19496  sylow2blem1  19517  gsumzres  19806  gsumzsplit  19824  gsumpr  19852  gsumzunsnd  19853  gsum2dlem2  19868  gsummptnn0fz  19883  dprd2da  19941  dpjidcl  19957  ablfac1b  19969  frlmsplit2  21698  psrass1lem  21857  coe1mul2lem2  22170  ofco2  22354  mdetralt  22511  mdetunilem9  22523  tgrest  23062  cmpfi  23311  fmss  23849  txflf  23909  tmdgsum  23998  tgpconncomp  24016  tsmssplit  24055  iscmet3lem3  25206  mbfss  25563  mbfadd  25578  mbfsub  25579  mbflimsup  25583  mbfmul  25643  itg2cnlem1  25678  ellimc2  25794  dvreslem  25826  dvres2lem  25827  dvidlem  25832  dvmptresicc  25833  dvcnp2  25837  dvcnp2OLD  25838  dvmulbr  25857  dvmulbrOLD  25858  dvcobr  25865  dvcobrOLD  25866  dvrec  25875  dvmptntr  25891  dvcnvlem  25896  lhop1lem  25934  lhop2  25936  itgparts  25970  itgsubstlem  25971  itgpowd  25973  plypf1  26133  taylthlem2  26298  taylthlem2OLD  26299  pserdvlem2  26354  abelth  26367  pige3ALT  26445  efifo  26472  eff1olem  26473  dvlog2  26578  resqrtcn  26675  sqrtcn  26676  dvatan  26861  rlimcnp2  26892  xrlimcnp  26894  efrlim  26895  efrlimOLD  26896  cxp2lim  26903  chpo1ub  27407  dchrisum0lem2a  27444  pnt2  27540  pnt  27541  wlknwwlksnbij  29851  ressnm  32919  gsummpt2d  33015  rmulccn  33894  xrge0mulc1cn  33907  gsumesum  34025  esumsnf  34030  esumcvg  34052  omsmon  34265  carsggect  34285  eulerpartlem1  34334  eulerpartgbij  34339  gsumnunsn  34508  cxpcncf1  34562  itgexpif  34573  reprpmtf1o  34593  elmsubrn  35500  divcnvlin  35705  mptsnunlem  37311  dissneqlem  37313  broucube  37633  mbfposadd  37646  itggt0cn  37669  ftc1anclem3  37674  ftc1anclem8  37679  dvasin  37683  dvacos  37684  areacirc  37692  sdclem2  37721  cncfres  37744  resopunitintvd  41999  resclunitintvd  42000  lcmineqlem2  42003  evlsbagval  42539  pwssplit4  43062  pwfi2f1o  43069  hbtlem6  43102  areaquad  43189  hashnzfzclim  44295  lhe4.4ex1a  44302  resmpti  45156  climresmpt  45641  dvcosre  45894  itgsinexplem1  45936  itgcoscmulx  45951  dirkeritg  46084  dirkercncflem2  46086  fourierdlem16  46105  fourierdlem21  46110  fourierdlem22  46111  fourierdlem57  46145  fourierdlem58  46146  fourierdlem62  46150  fourierdlem83  46171  fourierdlem111  46199  fouriersw  46213  0ome  46511