MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  resmpt Structured version   Visualization version   GIF version

Theorem resmpt 5899
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.
StepHypRef Expression
1 resopab2 5898 . 2 (𝐵𝐴 → ({⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐶)} ↾ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐵𝑦 = 𝐶)})
2 df-mpt 5139 . . 3 (𝑥𝐴𝐶) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐶)}
32reseq1i 5843 . 2 ((𝑥𝐴𝐶) ↾ 𝐵) = ({⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐶)} ↾ 𝐵)
4 df-mpt 5139 . 2 (𝑥𝐵𝐶) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐵𝑦 = 𝐶)}
51, 3, 43eqtr4g 2881 1 (𝐵𝐴 → ((𝑥𝐴𝐶) ↾ 𝐵) = (𝑥𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1528  wcel 2105  wss 3935  {copab 5120  cmpt 5138  cres 5551
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pr 5321
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3497  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-opab 5121  df-mpt 5139  df-xp 5555  df-rel 5556  df-res 5561
This theorem is referenced by:  resmpt3  5900  resmptf  5901  resmptd  5902  mptss  5904  fvresex  7652  f1stres  7704  f2ndres  7705  tposss  7884  dftpos2  7900  dftpos4  7902  resixpfo  8489  rlimresb  14912  lo1eq  14915  rlimeq  14916  fsumss  15072  isumclim3  15104  divcnvshft  15200  fprodss  15292  iprodclim3  15344  fprodefsum  15438  bitsf1ocnv  15783  conjsubg  18330  odf1o2  18629  sylow1lem2  18655  sylow2blem1  18676  gsumzres  18960  gsumzsplit  18978  gsumpr  19006  gsumzunsnd  19007  gsum2dlem2  19022  gsummptnn0fz  19037  dprd2da  19095  dpjidcl  19111  ablfac1b  19123  psrass1lem  20087  coe1mul2lem2  20366  frlmsplit2  20847  ofco2  20990  mdetralt  21147  mdetunilem9  21159  tgrest  21697  cmpfi  21946  fmss  22484  txflf  22544  tmdgsum  22633  tgpconncomp  22650  tsmssplit  22689  iscmet3lem3  23822  mbfss  24176  mbfadd  24191  mbfsub  24192  mbflimsup  24196  mbfmul  24256  itg2cnlem1  24291  ellimc2  24404  dvreslem  24436  dvres2lem  24437  dvidlem  24442  dvcnp2  24446  dvmulbr  24465  dvcobr  24472  dvrec  24481  dvmptntr  24497  dvcnvlem  24502  lhop1lem  24539  lhop2  24541  itgparts  24573  itgsubstlem  24574  tdeglem4  24583  plypf1  24731  taylthlem2  24891  pserdvlem2  24945  abelth  24958  pige3ALT  25034  efifo  25058  eff1olem  25059  dvlog2  25163  resqrtcn  25257  sqrtcn  25258  dvatan  25440  rlimcnp2  25472  xrlimcnp  25474  efrlim  25475  cxp2lim  25482  chpo1ub  25984  dchrisum0lem2a  26021  pnt2  26117  pnt  26118  wlknwwlksnbij  27594  elimampt  30312  ressnm  30566  gsummpt2d  30615  rmulccn  31071  xrge0mulc1cn  31084  gsumesum  31218  esumsnf  31223  esumcvg  31245  omsmon  31456  carsggect  31476  eulerpartlem1  31525  eulerpartgbij  31530  gsumnunsn  31711  cxpcncf1  31766  itgexpif  31777  reprpmtf1o  31797  elmsubrn  32673  divcnvlin  32862  mptsnunlem  34502  dissneqlem  34504  broucube  34808  mbfposadd  34821  itggt0cn  34846  ftc1anclem3  34851  ftc1anclem8  34856  dvasin  34860  dvacos  34861  areacirc  34869  sdclem2  34900  cncfres  34926  pwssplit4  39569  pwfi2f1o  39576  hbtlem6  39609  itgpowd  39701  areaquad  39703  hashnzfzclim  40534  lhe4.4ex1a  40541  resmpti  41314  climresmpt  41820  dvcosre  42076  dvmptresicc  42084  itgsinexplem1  42119  itgcoscmulx  42134  dirkeritg  42268  dirkercncflem2  42270  fourierdlem16  42289  fourierdlem21  42294  fourierdlem22  42295  fourierdlem57  42329  fourierdlem58  42330  fourierdlem62  42334  fourierdlem83  42355  fourierdlem111  42383  fouriersw  42397  0ome  42692
  Copyright terms: Public domain W3C validator