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

Theorem mpteq1 4889
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 2761 . . 3 (𝑥𝐴𝐶 = 𝐶)
21rgen 3060 . 2 𝑥𝐴 𝐶 = 𝐶
3 mpteq12 4888 . 2 ((𝐴 = 𝐵 ∧ ∀𝑥𝐴 𝐶 = 𝐶) → (𝑥𝐴𝐶) = (𝑥𝐵𝐶))
42, 3mpan2 709 1 (𝐴 = 𝐵 → (𝑥𝐴𝐶) = (𝑥𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1632  wcel 2139  wral 3050  cmpt 4881
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-ral 3055  df-opab 4865  df-mpt 4882
This theorem is referenced by:  mpteq1d  4890  mpteq1i  4891  fmptap  6601  mpt2mpt  6918  mpt2mptsx  7402  mpt2mpts  7403  tposf12  7547  oarec  7813  pwfseq  9698  wunex2  9772  wuncval2  9781  wrd2f1tovbij  13924  vrmdfval  17614  pmtrfval  18090  sylow1  18238  sylow2b  18258  sylow3lem5  18266  sylow3  18268  gsumconst  18554  gsum2dlem2  18590  gsumcom2  18594  srgbinomlem4  18763  mvrfval  19642  mplcoe1  19687  mplcoe5  19690  evlsval  19741  ply1coe  19888  coe1fzgsumd  19894  evls1fval  19906  evl1gsumd  19943  gsumfsum  20035  mavmul0  20580  m2detleiblem3  20657  m2detleiblem4  20658  madugsum  20671  cramer0  20718  pmatcollpw3fi1lem1  20813  restco  21190  cnmpt1t  21690  cnmpt2t  21698  fmval  21968  symgtgp  22126  prdstgpd  22149  dfarea  24907  istrkg2ld  25579  gsumvsca1  30112  gsumvsca2  30113  indv  30404  gsumesum  30451  esumlub  30452  esum2d  30485  sitg0  30738  matunitlindflem1  33736  matunitlindf  33738  sdclem2  33869  fsovcnvlem  38827  ntrneibex  38891  stoweidlem9  40747  sge0sn  41117  sge0iunmptlemfi  41151  sge0isum  41165  ovn02  41306
  Copyright terms: Public domain W3C validator