Theorem resmpt 6011

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109   ⊆ wss 3917  {copab 5172   ↦ cmpt 5191   ↾ cres 5643

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 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

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 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-opab 5173  df-mpt 5192  df-xp 5647  df-rel 5648  df-res 5653

This theorem is referenced by:  resmpt3  6012  resmptf  6013  resmptd  6014  mptss  6016  elimampt  6017  fvresex  7941  f1stres  7995  f2ndres  7996  tposss  8209  dftpos2  8225  dftpos4  8227  resixpfo  8912  rlimresb  15538  lo1eq  15541  rlimeq  15542  fsumss  15698  isumclim3  15732  divcnvshft  15828  fprodss  15921  iprodclim3  15973  fprodefsum  16068  bitsf1ocnv  16421  conjsubg  19189  odf1o2  19510  sylow1lem2  19536  sylow2blem1  19557  gsumzres  19846  gsumzsplit  19864  gsumpr  19892  gsumzunsnd  19893  gsum2dlem2  19908  gsummptnn0fz  19923  dprd2da  19981  dpjidcl  19997  ablfac1b  20009  frlmsplit2  21689  psrass1lem  21848  coe1mul2lem2  22161  ofco2  22345  mdetralt  22502  mdetunilem9  22514  tgrest  23053  cmpfi  23302  fmss  23840  txflf  23900  tmdgsum  23989  tgpconncomp  24007  tsmssplit  24046  iscmet3lem3  25197  mbfss  25554  mbfadd  25569  mbfsub  25570  mbflimsup  25574  mbfmul  25634  itg2cnlem1  25669  ellimc2  25785  dvreslem  25817  dvres2lem  25818  dvidlem  25823  dvmptresicc  25824  dvcnp2  25828  dvcnp2OLD  25829  dvmulbr  25848  dvmulbrOLD  25849  dvcobr  25856  dvcobrOLD  25857  dvrec  25866  dvmptntr  25882  dvcnvlem  25887  lhop1lem  25925  lhop2  25927  itgparts  25961  itgsubstlem  25962  itgpowd  25964  plypf1  26124  taylthlem2  26289  taylthlem2OLD  26290  pserdvlem2  26345  abelth  26358  pige3ALT  26436  efifo  26463  eff1olem  26464  dvlog2  26569  resqrtcn  26666  sqrtcn  26667  dvatan  26852  rlimcnp2  26883  xrlimcnp  26885  efrlim  26886  efrlimOLD  26887  cxp2lim  26894  chpo1ub  27398  dchrisum0lem2a  27435  pnt2  27531  pnt  27532  wlknwwlksnbij  29825  ressnm  32893  gsummpt2d  32996  rmulccn  33925  xrge0mulc1cn  33938  gsumesum  34056  esumsnf  34061  esumcvg  34083  omsmon  34296  carsggect  34316  eulerpartlem1  34365  eulerpartgbij  34370  gsumnunsn  34539  cxpcncf1  34593  itgexpif  34604  reprpmtf1o  34624  elmsubrn  35522  divcnvlin  35727  mptsnunlem  37333  dissneqlem  37335  broucube  37655  mbfposadd  37668  itggt0cn  37691  ftc1anclem3  37696  ftc1anclem8  37701  dvasin  37705  dvacos  37706  areacirc  37714  sdclem2  37743  cncfres  37766  resopunitintvd  42021  resclunitintvd  42022  lcmineqlem2  42025  evlsbagval  42561  pwssplit4  43085  pwfi2f1o  43092  hbtlem6  43125  areaquad  43212  hashnzfzclim  44318  lhe4.4ex1a  44325  resmpti  45179  climresmpt  45664  dvcosre  45917  itgsinexplem1  45959  itgcoscmulx  45974  dirkeritg  46107  dirkercncflem2  46109  fourierdlem16  46128  fourierdlem21  46133  fourierdlem22  46134  fourierdlem57  46168  fourierdlem58  46169  fourierdlem62  46173  fourierdlem83  46194  fourierdlem111  46222  fouriersw  46236  0ome  46534