Theorem resmpt 5948

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1539   ∈ wcel 2107   ⊆ wss 3888  {copab 5137   ↦ cmpt 5158   ↾ cres 5592

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-12 2172  ax-ext 2710  ax-sep 5224  ax-nul 5231  ax-pr 5353

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-opab 5138  df-mpt 5159  df-xp 5596  df-rel 5597  df-res 5602

This theorem is referenced by:  resmpt3  5949  resmptf  5950  resmptd  5951  mptss  5953  fvresex  7811  f1stres  7864  f2ndres  7865  tposss  8052  dftpos2  8068  dftpos4  8070  resixpfo  8733  rlimresb  15283  lo1eq  15286  rlimeq  15287  fsumss  15446  isumclim3  15480  divcnvshft  15576  fprodss  15667  iprodclim3  15719  fprodefsum  15813  bitsf1ocnv  16160  conjsubg  18875  odf1o2  19187  sylow1lem2  19213  sylow2blem1  19234  gsumzres  19519  gsumzsplit  19537  gsumpr  19565  gsumzunsnd  19566  gsum2dlem2  19581  gsummptnn0fz  19596  dprd2da  19654  dpjidcl  19670  ablfac1b  19682  frlmsplit2  20989  psrass1lemOLD  21152  psrass1lem  21155  coe1mul2lem2  21448  ofco2  21609  mdetralt  21766  mdetunilem9  21778  tgrest  22319  cmpfi  22568  fmss  23106  txflf  23166  tmdgsum  23255  tgpconncomp  23273  tsmssplit  23312  iscmet3lem3  24463  mbfss  24819  mbfadd  24834  mbfsub  24835  mbflimsup  24839  mbfmul  24900  itg2cnlem1  24935  ellimc2  25050  dvreslem  25082  dvres2lem  25083  dvidlem  25088  dvmptresicc  25089  dvcnp2  25093  dvmulbr  25112  dvcobr  25119  dvrec  25128  dvmptntr  25144  dvcnvlem  25149  lhop1lem  25186  lhop2  25188  itgparts  25220  itgsubstlem  25221  itgpowd  25223  tdeglem4OLD  25234  plypf1  25382  taylthlem2  25542  pserdvlem2  25596  abelth  25609  pige3ALT  25685  efifo  25712  eff1olem  25713  dvlog2  25817  resqrtcn  25911  sqrtcn  25912  dvatan  26094  rlimcnp2  26125  xrlimcnp  26127  efrlim  26128  cxp2lim  26135  chpo1ub  26637  dchrisum0lem2a  26674  pnt2  26770  pnt  26771  wlknwwlksnbij  28262  elimampt  30982  ressnm  31245  gsummpt2d  31318  rmulccn  31887  xrge0mulc1cn  31900  gsumesum  32036  esumsnf  32041  esumcvg  32063  omsmon  32274  carsggect  32294  eulerpartlem1  32343  eulerpartgbij  32348  gsumnunsn  32529  cxpcncf1  32584  itgexpif  32595  reprpmtf1o  32615  elmsubrn  33499  divcnvlin  33707  mptsnunlem  35518  dissneqlem  35520  broucube  35820  mbfposadd  35833  itggt0cn  35856  ftc1anclem3  35861  ftc1anclem8  35866  dvasin  35870  dvacos  35871  areacirc  35879  sdclem2  35909  cncfres  35932  resopunitintvd  40041  resclunitintvd  40042  lcmineqlem2  40045  pwssplit4  40921  pwfi2f1o  40928  hbtlem6  40961  areaquad  41054  hashnzfzclim  41947  lhe4.4ex1a  41954  resmpti  42721  climresmpt  43207  dvcosre  43460  itgsinexplem1  43502  itgcoscmulx  43517  dirkeritg  43650  dirkercncflem2  43652  fourierdlem16  43671  fourierdlem21  43676  fourierdlem22  43677  fourierdlem57  43711  fourierdlem58  43712  fourierdlem62  43716  fourierdlem83  43737  fourierdlem111  43765  fouriersw  43779  0ome  44074