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

Theorem resmpt 5352
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 5351 . 2 (𝐵𝐴 → ({⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐶)} ↾ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐵𝑦 = 𝐶)})
2 df-mpt 4635 . . 3 (𝑥𝐴𝐶) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐶)}
32reseq1i 5296 . 2 ((𝑥𝐴𝐶) ↾ 𝐵) = ({⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐶)} ↾ 𝐵)
4 df-mpt 4635 . 2 (𝑥𝐵𝐶) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐵𝑦 = 𝐶)}
51, 3, 43eqtr4g 2664 1 (𝐵𝐴 → ((𝑥𝐴𝐶) ↾ 𝐵) = (𝑥𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382   = wceq 1474  wcel 1975  wss 3535  {copab 4632  cmpt 4633  cres 5026
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-9 1984  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585  ax-sep 4699  ax-nul 4708  ax-pr 4824
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-clab 2592  df-cleq 2598  df-clel 2601  df-nfc 2735  df-ral 2896  df-rex 2897  df-rab 2900  df-v 3170  df-dif 3538  df-un 3540  df-in 3542  df-ss 3549  df-nul 3870  df-if 4032  df-sn 4121  df-pr 4123  df-op 4127  df-opab 4634  df-mpt 4635  df-xp 5030  df-rel 5031  df-res 5036
This theorem is referenced by:  resmpt3  5353  resmptd  5354  mptss  5356  fvresex  7005  f1stres  7054  f2ndres  7055  tposss  7213  dftpos2  7229  dftpos4  7231  resixpfo  7805  rlimresb  14086  lo1eq  14089  rlimeq  14090  fsumss  14245  isumclim3  14274  divcnvshft  14368  fprodss  14459  iprodclim3  14512  fprodefsum  14606  bitsf1ocnv  14946  conjsubg  17457  psgnunilem5  17679  odf1o2  17753  sylow1lem2  17779  sylow2blem1  17800  gsumzres  18075  gsumzsplit  18092  gsumzunsnd  18120  gsum2dlem2  18135  gsummptnn0fz  18147  dprd2da  18206  dpjidcl  18222  ablfac1b  18234  psrass1lem  19140  coe1mul2lem2  19401  frlmsplit2  19869  ofco2  20014  mdetralt  20171  mdetunilem9  20183  tgrest  20711  cmpfi  20959  cnmptid  21212  fmss  21498  txflf  21558  tmdgsum  21647  tgpconcomp  21664  tsmssplit  21703  iscmet3lem3  22810  mbfss  23132  mbfadd  23147  mbfsub  23148  mbflimsup  23152  mbfmul  23212  itg2cnlem1  23247  ellimc2  23360  dvreslem  23392  dvres2lem  23393  dvidlem  23398  dvcnp2  23402  dvmulbr  23421  dvcobr  23428  dvrec  23437  dvmptntr  23453  dvcnvlem  23456  lhop1lem  23493  lhop2  23495  itgparts  23527  itgsubstlem  23528  tdeglem4  23537  plypf1  23685  taylthlem2  23845  pserdvlem2  23899  abelth  23912  pige3  23986  efifo  24010  eff1olem  24011  dvlog2  24112  resqrtcn  24203  sqrtcn  24204  dvatan  24375  rlimcnp2  24406  xrlimcnp  24408  efrlim  24409  cxp2lim  24416  chpo1ub  24882  dchrisum0lem2a  24919  pnt2  25015  pnt  25016  resmptf  28640  ressnm  28784  gsummpt2d  28914  rmulccn  29104  xrge0mulc1cn  29117  gsumesum  29250  esumsnf  29255  esumcvg  29277  omsmon  29489  carsggect  29509  eulerpartlem1  29558  eulerpartgbij  29563  gsumnunsn  29744  elmsubrn  30481  divcnvlin  30673  mptsnunlem  32160  dissneqlem  32162  broucube  32412  mbfposadd  32426  itggt0cn  32451  ftc1anclem3  32456  ftc1anclem8  32461  dvasin  32465  dvacos  32466  areacirc  32474  sdclem2  32507  cncfres  32533  pwssplit4  36476  pwfi2f1o  36483  hbtlem6  36517  itgpowd  36618  areaquad  36620  hashnzfzclim  37342  lhe4.4ex1a  37349  resmpti  38153  climresmpt  38526  dvcosre  38599  dvmptresicc  38609  itgsinexplem1  38645  itgcoscmulx  38661  dirkeritg  38795  dirkercncflem2  38797  fourierdlem16  38816  fourierdlem21  38821  fourierdlem22  38822  fourierdlem57  38856  fourierdlem58  38857  fourierdlem62  38861  fourierdlem83  38882  fourierdlem111  38910  fouriersw  38924  0ome  39219  gsumpr  41930
  Copyright terms: Public domain W3C validator