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

Theorem resmpt 5996
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 5995 . 2 (𝐵𝐴 → ({⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐶)} ↾ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐵𝑦 = 𝐶)})
2 df-mpt 5194 . . 3 (𝑥𝐴𝐶) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐶)}
32reseq1i 5938 . 2 ((𝑥𝐴𝐶) ↾ 𝐵) = ({⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐶)} ↾ 𝐵)
4 df-mpt 5194 . 2 (𝑥𝐵𝐶) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐵𝑦 = 𝐶)}
51, 3, 43eqtr4g 2802 1 (𝐵𝐴 → ((𝑥𝐴𝐶) ↾ 𝐵) = (𝑥𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397   = wceq 1542  wcel 2107  wss 3915  {copab 5172  cmpt 5193  cres 5640
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 2708  ax-sep 5261  ax-nul 5268  ax-pr 5389
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-rab 3411  df-v 3450  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-opab 5173  df-mpt 5194  df-xp 5644  df-rel 5645  df-res 5650
This theorem is referenced by:  resmpt3  5997  resmptf  5998  resmptd  5999  mptss  6001  fvresex  7897  f1stres  7950  f2ndres  7951  tposss  8163  dftpos2  8179  dftpos4  8181  resixpfo  8881  rlimresb  15454  lo1eq  15457  rlimeq  15458  fsumss  15617  isumclim3  15651  divcnvshft  15747  fprodss  15838  iprodclim3  15890  fprodefsum  15984  bitsf1ocnv  16331  conjsubg  19047  odf1o2  19362  sylow1lem2  19388  sylow2blem1  19409  gsumzres  19693  gsumzsplit  19711  gsumpr  19739  gsumzunsnd  19740  gsum2dlem2  19755  gsummptnn0fz  19770  dprd2da  19828  dpjidcl  19844  ablfac1b  19856  frlmsplit2  21195  psrass1lemOLD  21358  psrass1lem  21361  coe1mul2lem2  21655  ofco2  21816  mdetralt  21973  mdetunilem9  21985  tgrest  22526  cmpfi  22775  fmss  23313  txflf  23373  tmdgsum  23462  tgpconncomp  23480  tsmssplit  23519  iscmet3lem3  24670  mbfss  25026  mbfadd  25041  mbfsub  25042  mbflimsup  25046  mbfmul  25107  itg2cnlem1  25142  ellimc2  25257  dvreslem  25289  dvres2lem  25290  dvidlem  25295  dvmptresicc  25296  dvcnp2  25300  dvmulbr  25319  dvcobr  25326  dvrec  25335  dvmptntr  25351  dvcnvlem  25356  lhop1lem  25393  lhop2  25395  itgparts  25427  itgsubstlem  25428  itgpowd  25430  tdeglem4OLD  25441  plypf1  25589  taylthlem2  25749  pserdvlem2  25803  abelth  25816  pige3ALT  25892  efifo  25919  eff1olem  25920  dvlog2  26024  resqrtcn  26118  sqrtcn  26119  dvatan  26301  rlimcnp2  26332  xrlimcnp  26334  efrlim  26335  cxp2lim  26342  chpo1ub  26844  dchrisum0lem2a  26881  pnt2  26977  pnt  26978  wlknwwlksnbij  28875  elimampt  31594  ressnm  31860  gsummpt2d  31933  rmulccn  32549  xrge0mulc1cn  32562  gsumesum  32698  esumsnf  32703  esumcvg  32725  omsmon  32938  carsggect  32958  eulerpartlem1  33007  eulerpartgbij  33012  gsumnunsn  33193  cxpcncf1  33248  itgexpif  33259  reprpmtf1o  33279  elmsubrn  34162  divcnvlin  34344  mptsnunlem  35838  dissneqlem  35840  broucube  36141  mbfposadd  36154  itggt0cn  36177  ftc1anclem3  36182  ftc1anclem8  36187  dvasin  36191  dvacos  36192  areacirc  36200  sdclem2  36230  cncfres  36253  resopunitintvd  40512  resclunitintvd  40513  lcmineqlem2  40516  pwssplit4  41445  pwfi2f1o  41452  hbtlem6  41485  areaquad  41579  hashnzfzclim  42676  lhe4.4ex1a  42683  resmpti  43469  climresmpt  43974  dvcosre  44227  itgsinexplem1  44269  itgcoscmulx  44284  dirkeritg  44417  dirkercncflem2  44419  fourierdlem16  44438  fourierdlem21  44443  fourierdlem22  44444  fourierdlem57  44478  fourierdlem58  44479  fourierdlem62  44483  fourierdlem83  44504  fourierdlem111  44532  fouriersw  44546  0ome  44844
  Copyright terms: Public domain W3C validator