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

Theorem resmpt 5437
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 5436 . 2 (𝐵𝐴 → ({⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐶)} ↾ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐵𝑦 = 𝐶)})
2 df-mpt 4721 . . 3 (𝑥𝐴𝐶) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐶)}
32reseq1i 5381 . 2 ((𝑥𝐴𝐶) ↾ 𝐵) = ({⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐶)} ↾ 𝐵)
4 df-mpt 4721 . 2 (𝑥𝐵𝐶) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐵𝑦 = 𝐶)}
51, 3, 43eqtr4g 2679 1 (𝐵𝐴 → ((𝑥𝐴𝐶) ↾ 𝐵) = (𝑥𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384   = wceq 1481  wcel 1988  wss 3567  {copab 4703  cmpt 4720  cres 5106
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-sep 4772  ax-nul 4780  ax-pr 4897
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-rab 2918  df-v 3197  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-sn 4169  df-pr 4171  df-op 4175  df-opab 4704  df-mpt 4721  df-xp 5110  df-rel 5111  df-res 5116
This theorem is referenced by:  resmpt3  5438  resmptf  5439  resmptd  5440  mptss  5442  fvresex  7124  f1stres  7175  f2ndres  7176  tposss  7338  dftpos2  7354  dftpos4  7356  resixpfo  7931  rlimresb  14277  lo1eq  14280  rlimeq  14281  fsumss  14437  isumclim3  14471  divcnvshft  14568  fprodss  14659  iprodclim3  14712  fprodefsum  14806  bitsf1ocnv  15147  conjsubg  17673  psgnunilem5  17895  odf1o2  17969  sylow1lem2  17995  sylow2blem1  18016  gsumzres  18291  gsumzsplit  18308  gsumzunsnd  18336  gsum2dlem2  18351  gsummptnn0fz  18363  dprd2da  18422  dpjidcl  18438  ablfac1b  18450  psrass1lem  19358  coe1mul2lem2  19619  frlmsplit2  20093  ofco2  20238  mdetralt  20395  mdetunilem9  20407  tgrest  20944  cmpfi  21192  cnmptid  21445  fmss  21731  txflf  21791  tmdgsum  21880  tgpconncomp  21897  tsmssplit  21936  iscmet3lem3  23069  mbfss  23394  mbfadd  23409  mbfsub  23410  mbflimsup  23414  mbfmul  23474  itg2cnlem1  23509  ellimc2  23622  dvreslem  23654  dvres2lem  23655  dvidlem  23660  dvcnp2  23664  dvmulbr  23683  dvcobr  23690  dvrec  23699  dvmptntr  23715  dvcnvlem  23720  lhop1lem  23757  lhop2  23759  itgparts  23791  itgsubstlem  23792  tdeglem4  23801  plypf1  23949  taylthlem2  24109  pserdvlem2  24163  abelth  24176  pige3  24250  efifo  24274  eff1olem  24275  dvlog2  24380  resqrtcn  24471  sqrtcn  24472  dvatan  24643  rlimcnp2  24674  xrlimcnp  24676  efrlim  24677  cxp2lim  24684  chpo1ub  25150  dchrisum0lem2a  25187  pnt2  25283  pnt  25284  elimampt  29411  ressnm  29625  gsummpt2d  29755  rmulccn  29948  xrge0mulc1cn  29961  gsumesum  30095  esumsnf  30100  esumcvg  30122  omsmon  30334  carsggect  30354  eulerpartlem1  30403  eulerpartgbij  30408  gsumnunsn  30589  cxpcncf1  30647  itgexpif  30658  reprpmtf1o  30678  elmsubrn  31399  divcnvlin  31593  mptsnunlem  33156  dissneqlem  33158  broucube  33414  mbfposadd  33428  itggt0cn  33453  ftc1anclem3  33458  ftc1anclem8  33463  dvasin  33467  dvacos  33468  areacirc  33476  sdclem2  33509  cncfres  33535  pwssplit4  37478  pwfi2f1o  37485  hbtlem6  37518  itgpowd  37619  areaquad  37621  hashnzfzclim  38341  lhe4.4ex1a  38348  resmpti  39175  climresmpt  39691  dvcosre  39889  dvmptresicc  39897  itgsinexplem1  39932  itgcoscmulx  39948  dirkeritg  40082  dirkercncflem2  40084  fourierdlem16  40103  fourierdlem21  40108  fourierdlem22  40109  fourierdlem57  40143  fourierdlem58  40144  fourierdlem62  40148  fourierdlem83  40169  fourierdlem111  40197  fouriersw  40211  0ome  40506  gsumpr  41904
  Copyright terms: Public domain W3C validator