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

Theorem resmpt 5876
 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 5875 . 2 (𝐵𝐴 → ({⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐶)} ↾ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐵𝑦 = 𝐶)})
2 df-mpt 5114 . . 3 (𝑥𝐴𝐶) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐶)}
32reseq1i 5818 . 2 ((𝑥𝐴𝐶) ↾ 𝐵) = ({⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐶)} ↾ 𝐵)
4 df-mpt 5114 . 2 (𝑥𝐵𝐶) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐵𝑦 = 𝐶)}
51, 3, 43eqtr4g 2861 1 (𝐵𝐴 → ((𝑥𝐴𝐶) ↾ 𝐵) = (𝑥𝐵𝐶))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538   ∈ wcel 2112   ⊆ wss 3884  {copab 5095   ↦ cmpt 5113   ↾ cres 5525 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 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-sep 5170  ax-nul 5177  ax-pr 5298 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-rab 3118  df-v 3446  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4247  df-if 4429  df-sn 4529  df-pr 4531  df-op 4535  df-opab 5096  df-mpt 5114  df-xp 5529  df-rel 5530  df-res 5535 This theorem is referenced by:  resmpt3  5877  resmptf  5878  resmptd  5879  mptss  5881  fvresex  7647  f1stres  7699  f2ndres  7700  tposss  7880  dftpos2  7896  dftpos4  7898  resixpfo  8487  rlimresb  14917  lo1eq  14920  rlimeq  14921  fsumss  15077  isumclim3  15109  divcnvshft  15205  fprodss  15297  iprodclim3  15349  fprodefsum  15443  bitsf1ocnv  15786  conjsubg  18385  odf1o2  18693  sylow1lem2  18719  sylow2blem1  18740  gsumzres  19025  gsumzsplit  19043  gsumpr  19071  gsumzunsnd  19072  gsum2dlem2  19087  gsummptnn0fz  19102  dprd2da  19160  dpjidcl  19176  ablfac1b  19188  frlmsplit2  20465  psrass1lem  20618  coe1mul2lem2  20900  ofco2  21059  mdetralt  21216  mdetunilem9  21228  tgrest  21767  cmpfi  22016  fmss  22554  txflf  22614  tmdgsum  22703  tgpconncomp  22721  tsmssplit  22760  iscmet3lem3  23897  mbfss  24253  mbfadd  24268  mbfsub  24269  mbflimsup  24273  mbfmul  24333  itg2cnlem1  24368  ellimc2  24483  dvreslem  24515  dvres2lem  24516  dvidlem  24521  dvmptresicc  24522  dvcnp2  24526  dvmulbr  24545  dvcobr  24552  dvrec  24561  dvmptntr  24577  dvcnvlem  24582  lhop1lem  24619  lhop2  24621  itgparts  24653  itgsubstlem  24654  itgpowd  24656  tdeglem4  24664  plypf1  24812  taylthlem2  24972  pserdvlem2  25026  abelth  25039  pige3ALT  25115  efifo  25142  eff1olem  25143  dvlog2  25247  resqrtcn  25341  sqrtcn  25342  dvatan  25524  rlimcnp2  25555  xrlimcnp  25557  efrlim  25558  cxp2lim  25565  chpo1ub  26067  dchrisum0lem2a  26104  pnt2  26200  pnt  26201  wlknwwlksnbij  27677  elimampt  30400  ressnm  30667  gsummpt2d  30737  rmulccn  31279  xrge0mulc1cn  31292  gsumesum  31426  esumsnf  31431  esumcvg  31453  omsmon  31664  carsggect  31684  eulerpartlem1  31733  eulerpartgbij  31738  gsumnunsn  31919  cxpcncf1  31974  itgexpif  31985  reprpmtf1o  32005  elmsubrn  32883  divcnvlin  33072  mptsnunlem  34750  dissneqlem  34752  broucube  35084  mbfposadd  35097  itggt0cn  35120  ftc1anclem3  35125  ftc1anclem8  35130  dvasin  35134  dvacos  35135  areacirc  35143  sdclem2  35173  cncfres  35196  resopunitintvd  39307  resclunitintvd  39308  lcmineqlem2  39311  pwssplit4  40020  pwfi2f1o  40027  hbtlem6  40060  areaquad  40153  hashnzfzclim  41013  lhe4.4ex1a  41020  resmpti  41789  climresmpt  42288  dvcosre  42541  itgsinexplem1  42583  itgcoscmulx  42598  dirkeritg  42731  dirkercncflem2  42733  fourierdlem16  42752  fourierdlem21  42757  fourierdlem22  42758  fourierdlem57  42792  fourierdlem58  42793  fourierdlem62  42797  fourierdlem83  42818  fourierdlem111  42846  fouriersw  42860  0ome  43155
 Copyright terms: Public domain W3C validator