Theorem resmpt 5890

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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1543   ∈ wcel 2112   ⊆ wss 3853  {copab 5101   ↦ cmpt 5120   ↾ cres 5538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-10 2143  ax-12 2177  ax-ext 2708  ax-sep 5177  ax-nul 5184  ax-pr 5307

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-rab 3060  df-v 3400  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-nul 4224  df-if 4426  df-sn 4528  df-pr 4530  df-op 4534  df-opab 5102  df-mpt 5121  df-xp 5542  df-rel 5543  df-res 5548

This theorem is referenced by:  resmpt3  5891  resmptf  5892  resmptd  5893  mptss  5895  fvresex  7711  f1stres  7763  f2ndres  7764  tposss  7947  dftpos2  7963  dftpos4  7965  resixpfo  8595  rlimresb  15091  lo1eq  15094  rlimeq  15095  fsumss  15254  isumclim3  15286  divcnvshft  15382  fprodss  15473  iprodclim3  15525  fprodefsum  15619  bitsf1ocnv  15966  conjsubg  18608  odf1o2  18916  sylow1lem2  18942  sylow2blem1  18963  gsumzres  19248  gsumzsplit  19266  gsumpr  19294  gsumzunsnd  19295  gsum2dlem2  19310  gsummptnn0fz  19325  dprd2da  19383  dpjidcl  19399  ablfac1b  19411  frlmsplit2  20689  psrass1lemOLD  20853  psrass1lem  20856  coe1mul2lem2  21143  ofco2  21302  mdetralt  21459  mdetunilem9  21471  tgrest  22010  cmpfi  22259  fmss  22797  txflf  22857  tmdgsum  22946  tgpconncomp  22964  tsmssplit  23003  iscmet3lem3  24141  mbfss  24497  mbfadd  24512  mbfsub  24513  mbflimsup  24517  mbfmul  24578  itg2cnlem1  24613  ellimc2  24728  dvreslem  24760  dvres2lem  24761  dvidlem  24766  dvmptresicc  24767  dvcnp2  24771  dvmulbr  24790  dvcobr  24797  dvrec  24806  dvmptntr  24822  dvcnvlem  24827  lhop1lem  24864  lhop2  24866  itgparts  24898  itgsubstlem  24899  itgpowd  24901  tdeglem4OLD  24912  plypf1  25060  taylthlem2  25220  pserdvlem2  25274  abelth  25287  pige3ALT  25363  efifo  25390  eff1olem  25391  dvlog2  25495  resqrtcn  25589  sqrtcn  25590  dvatan  25772  rlimcnp2  25803  xrlimcnp  25805  efrlim  25806  cxp2lim  25813  chpo1ub  26315  dchrisum0lem2a  26352  pnt2  26448  pnt  26449  wlknwwlksnbij  27926  elimampt  30646  ressnm  30910  gsummpt2d  30982  rmulccn  31546  xrge0mulc1cn  31559  gsumesum  31693  esumsnf  31698  esumcvg  31720  omsmon  31931  carsggect  31951  eulerpartlem1  32000  eulerpartgbij  32005  gsumnunsn  32186  cxpcncf1  32241  itgexpif  32252  reprpmtf1o  32272  elmsubrn  33157  divcnvlin  33367  mptsnunlem  35195  dissneqlem  35197  broucube  35497  mbfposadd  35510  itggt0cn  35533  ftc1anclem3  35538  ftc1anclem8  35543  dvasin  35547  dvacos  35548  areacirc  35556  sdclem2  35586  cncfres  35609  resopunitintvd  39717  resclunitintvd  39718  lcmineqlem2  39721  pwssplit4  40558  pwfi2f1o  40565  hbtlem6  40598  areaquad  40691  hashnzfzclim  41554  lhe4.4ex1a  41561  resmpti  42328  climresmpt  42818  dvcosre  43071  itgsinexplem1  43113  itgcoscmulx  43128  dirkeritg  43261  dirkercncflem2  43263  fourierdlem16  43282  fourierdlem21  43287  fourierdlem22  43288  fourierdlem57  43322  fourierdlem58  43323  fourierdlem62  43327  fourierdlem83  43348  fourierdlem111  43376  fouriersw  43390  0ome  43685