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

Theorem resmpt 5484
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 5483 . 2 (𝐵𝐴 → ({⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐶)} ↾ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐵𝑦 = 𝐶)})
2 df-mpt 4763 . . 3 (𝑥𝐴𝐶) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐶)}
32reseq1i 5424 . 2 ((𝑥𝐴𝐶) ↾ 𝐵) = ({⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐶)} ↾ 𝐵)
4 df-mpt 4763 . 2 (𝑥𝐵𝐶) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐵𝑦 = 𝐶)}
51, 3, 43eqtr4g 2710 1 (𝐵𝐴 → ((𝑥𝐴𝐶) ↾ 𝐵) = (𝑥𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383   = wceq 1523  wcel 2030  wss 3607  {copab 4745  cmpt 4762  cres 5145
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pr 4936
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-opab 4746  df-mpt 4763  df-xp 5149  df-rel 5150  df-res 5155
This theorem is referenced by:  resmpt3  5485  resmptf  5486  resmptd  5487  mptss  5489  fvresex  7181  f1stres  7234  f2ndres  7235  tposss  7398  dftpos2  7414  dftpos4  7416  resixpfo  7988  rlimresb  14340  lo1eq  14343  rlimeq  14344  fsumss  14500  isumclim3  14534  divcnvshft  14631  fprodss  14722  iprodclim3  14775  fprodefsum  14869  bitsf1ocnv  15213  conjsubg  17739  psgnunilem5  17960  odf1o2  18034  sylow1lem2  18060  sylow2blem1  18081  gsumzres  18356  gsumzsplit  18373  gsumzunsnd  18401  gsum2dlem2  18416  gsummptnn0fz  18428  dprd2da  18487  dpjidcl  18503  ablfac1b  18515  psrass1lem  19425  coe1mul2lem2  19686  frlmsplit2  20160  ofco2  20305  mdetralt  20462  mdetunilem9  20474  tgrest  21011  cmpfi  21259  cnmptid  21512  fmss  21797  txflf  21857  tmdgsum  21946  tgpconncomp  21963  tsmssplit  22002  iscmet3lem3  23134  mbfss  23458  mbfadd  23473  mbfsub  23474  mbflimsup  23478  mbfmul  23538  itg2cnlem1  23573  ellimc2  23686  dvreslem  23718  dvres2lem  23719  dvidlem  23724  dvcnp2  23728  dvmulbr  23747  dvcobr  23754  dvrec  23763  dvmptntr  23779  dvcnvlem  23784  lhop1lem  23821  lhop2  23823  itgparts  23855  itgsubstlem  23856  tdeglem4  23865  plypf1  24013  taylthlem2  24173  pserdvlem2  24227  abelth  24240  pige3  24314  efifo  24338  eff1olem  24339  dvlog2  24444  resqrtcn  24535  sqrtcn  24536  dvatan  24707  rlimcnp2  24738  xrlimcnp  24740  efrlim  24741  cxp2lim  24748  chpo1ub  25214  dchrisum0lem2a  25251  pnt2  25347  pnt  25348  elimampt  29566  ressnm  29779  gsummpt2d  29909  rmulccn  30102  xrge0mulc1cn  30115  gsumesum  30249  esumsnf  30254  esumcvg  30276  omsmon  30488  carsggect  30508  eulerpartlem1  30557  eulerpartgbij  30562  gsumnunsn  30743  cxpcncf1  30801  itgexpif  30812  reprpmtf1o  30832  elmsubrn  31551  divcnvlin  31744  mptsnunlem  33315  dissneqlem  33317  broucube  33573  mbfposadd  33587  itggt0cn  33612  ftc1anclem3  33617  ftc1anclem8  33622  dvasin  33626  dvacos  33627  areacirc  33635  sdclem2  33668  cncfres  33694  pwssplit4  37976  pwfi2f1o  37983  hbtlem6  38016  itgpowd  38117  areaquad  38119  hashnzfzclim  38838  lhe4.4ex1a  38845  resmpti  39673  climresmpt  40209  dvcosre  40444  dvmptresicc  40452  itgsinexplem1  40487  itgcoscmulx  40503  dirkeritg  40637  dirkercncflem2  40639  fourierdlem16  40658  fourierdlem21  40663  fourierdlem22  40664  fourierdlem57  40698  fourierdlem58  40699  fourierdlem62  40703  fourierdlem83  40724  fourierdlem111  40752  fouriersw  40766  0ome  41064  gsumpr  42464
  Copyright terms: Public domain W3C validator