Theorem resmpt 6004

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114   ⊆ wss 3903  {copab 5162   ↦ cmpt 5181   ↾ cres 5634

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 2709  ax-sep 5243  ax-pr 5379

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 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-opab 5163  df-mpt 5182  df-xp 5638  df-rel 5639  df-res 5644

This theorem is referenced by:  resmpt3  6005  resmptf  6006  resmptd  6007  mptss  6009  elimampt  6010  fvresex  7914  f1stres  7967  f2ndres  7968  tposss  8179  dftpos2  8195  dftpos4  8197  resixpfo  8886  rlimresb  15500  lo1eq  15503  rlimeq  15504  fsumss  15660  isumclim3  15694  divcnvshft  15790  fprodss  15883  iprodclim3  15935  fprodefsum  16030  bitsf1ocnv  16383  conjsubg  19191  odf1o2  19514  sylow1lem2  19540  sylow2blem1  19561  gsumzres  19850  gsumzsplit  19868  gsumpr  19896  gsumzunsnd  19897  gsum2dlem2  19912  gsummptnn0fz  19927  dprd2da  19985  dpjidcl  20001  ablfac1b  20013  frlmsplit2  21740  psrass1lem  21900  coe1mul2lem2  22222  ofco2  22407  mdetralt  22564  mdetunilem9  22576  tgrest  23115  cmpfi  23364  fmss  23902  txflf  23962  tmdgsum  24051  tgpconncomp  24069  tsmssplit  24108  iscmet3lem3  25258  mbfss  25615  mbfadd  25630  mbfsub  25631  mbflimsup  25635  mbfmul  25695  itg2cnlem1  25730  ellimc2  25846  dvreslem  25878  dvres2lem  25879  dvidlem  25884  dvmptresicc  25885  dvcnp2  25889  dvcnp2OLD  25890  dvmulbr  25909  dvmulbrOLD  25910  dvcobr  25917  dvcobrOLD  25918  dvrec  25927  dvmptntr  25943  dvcnvlem  25948  lhop1lem  25986  lhop2  25988  itgparts  26022  itgsubstlem  26023  itgpowd  26025  plypf1  26185  taylthlem2  26350  taylthlem2OLD  26351  pserdvlem2  26406  abelth  26419  pige3ALT  26497  efifo  26524  eff1olem  26525  dvlog2  26630  resqrtcn  26727  sqrtcn  26728  dvatan  26913  rlimcnp2  26944  xrlimcnp  26946  efrlim  26947  efrlimOLD  26948  cxp2lim  26955  chpo1ub  27459  dchrisum0lem2a  27496  pnt2  27592  pnt  27593  wlknwwlksnbij  29973  ressnm  33056  gsummpt2d  33142  rmulccn  34105  xrge0mulc1cn  34118  gsumesum  34236  esumsnf  34241  esumcvg  34263  omsmon  34475  carsggect  34495  eulerpartlem1  34544  eulerpartgbij  34549  gsumnunsn  34718  cxpcncf1  34772  itgexpif  34783  reprpmtf1o  34803  elmsubrn  35741  divcnvlin  35946  mptsnunlem  37587  dissneqlem  37589  broucube  37899  mbfposadd  37912  itggt0cn  37935  ftc1anclem3  37940  ftc1anclem8  37945  dvasin  37949  dvacos  37950  areacirc  37958  sdclem2  37987  cncfres  38010  resopunitintvd  42390  resclunitintvd  42391  lcmineqlem2  42394  evlsbagval  42921  pwssplit4  43440  pwfi2f1o  43447  hbtlem6  43480  areaquad  43567  hashnzfzclim  44672  lhe4.4ex1a  44679  resmpti  45531  climresmpt  46011  dvcosre  46264  itgsinexplem1  46306  itgcoscmulx  46321  dirkeritg  46454  dirkercncflem2  46456  fourierdlem16  46475  fourierdlem21  46480  fourierdlem22  46481  fourierdlem57  46515  fourierdlem58  46516  fourierdlem62  46520  fourierdlem83  46541  fourierdlem111  46569  fouriersw  46583  0ome  46881