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

Theorem mpteq1 4707
Description: An equality theorem for the maps to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)
Assertion
Ref Expression
mpteq1 (𝐴 = 𝐵 → (𝑥𝐴𝐶) = (𝑥𝐵𝐶))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵
Allowed substitution hint:   𝐶(𝑥)

Proof of Theorem mpteq1
StepHypRef Expression
1 eqidd 2622 . . 3 (𝑥𝐴𝐶 = 𝐶)
21rgen 2918 . 2 𝑥𝐴 𝐶 = 𝐶
3 mpteq12 4706 . 2 ((𝐴 = 𝐵 ∧ ∀𝑥𝐴 𝐶 = 𝐶) → (𝑥𝐴𝐶) = (𝑥𝐵𝐶))
42, 3mpan2 706 1 (𝐴 = 𝐵 → (𝑥𝐴𝐶) = (𝑥𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1480  wcel 1987  wral 2908  cmpt 4683
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-ral 2913  df-opab 4684  df-mpt 4685
This theorem is referenced by:  mpteq1d  4708  mpteq1i  4709  fmptap  6401  mpt2mpt  6717  mpt2mptsx  7193  mpt2mpts  7194  tposf12  7337  oarec  7602  pwfseq  9446  wunex2  9520  wuncval2  9529  wrd2f1tovbij  13653  vrmdfval  17333  pmtrfval  17810  sylow1  17958  sylow2b  17978  sylow3lem5  17986  sylow3  17988  gsumconst  18274  gsum2dlem2  18310  gsumcom2  18314  srgbinomlem4  18483  mvrfval  19360  mplcoe1  19405  mplcoe5  19408  evlsval  19459  ply1coe  19606  coe1fzgsumd  19612  evls1fval  19624  evl1gsumd  19661  gsumfsum  19753  mavmul0  20298  m2detleiblem3  20375  m2detleiblem4  20376  madugsum  20389  cramer0  20436  pmatcollpw3fi1lem1  20531  restco  20908  cnmpt1t  21408  cnmpt2t  21416  fmval  21687  symgtgp  21845  prdstgpd  21868  dfarea  24621  istrkg2ld  25293  gsumvsca1  29609  gsumvsca2  29610  indv  29898  gsumesum  29944  esumlub  29945  esum2d  29978  sitg0  30231  matunitlindflem1  33076  matunitlindf  33078  sdclem2  33209  fsovcnvlem  37828  ntrneibex  37892  stoweidlem9  39563  sge0sn  39933  sge0iunmptlemfi  39967  sge0isum  39981  ovn02  40119
  Copyright terms: Public domain W3C validator