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

Theorem mpteq1 5128
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 2740 . . 3 (𝑥𝐴𝐶 = 𝐶)
21rgen 3064 . 2 𝑥𝐴 𝐶 = 𝐶
3 mpteq12 5127 . 2 ((𝐴 = 𝐵 ∧ ∀𝑥𝐴 𝐶 = 𝐶) → (𝑥𝐴𝐶) = (𝑥𝐵𝐶))
42, 3mpan2 691 1 (𝐴 = 𝐵 → (𝑥𝐴𝐶) = (𝑥𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542  wcel 2114  wral 3054  cmpt 5120
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-10 2145  ax-12 2179  ax-ext 2711
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-tru 1545  df-ex 1787  df-nf 1791  df-sb 2075  df-clab 2718  df-cleq 2731  df-clel 2812  df-ral 3059  df-opab 5103  df-mpt 5121
This theorem is referenced by:  mpteq1d  5129  mpteq1i  5130  tposf12  7959  oarec  8232  wunex2  10251  wuncval2  10260  vrmdfval  18150  pmtrfval  18709  sylow1  18859  sylow2b  18879  sylow3lem5  18887  sylow3  18889  gsumconst  19186  gsum2dlem2  19223  gsumfsum  20297  mvrfval  20812  mplcoe1  20861  mplcoe5  20864  evlsval  20913  coe1fzgsumd  21090  evls1fval  21102  evl1gsumd  21140  mavmul0  21316  madugsum  21407  cramer0  21454  cnmpt1t  22429  cnmpt2t  22437  fmval  22707  symgtgp  22870  prdstgpd  22889  gsumvsca1  31069  gsumvsca2  31070  qusima  31179  nsgmgc  31182  nsgqusf1olem2  31184  indv  31563  gsumesum  31610  esumlub  31611  esum2d  31644  sitg0  31896  matunitlindflem1  35429  matunitlindf  35431  sdclem2  35556  fsovcnvlem  41208  ntrneibex  41270  stoweidlem9  43133  sge0sn  43500  sge0iunmptlemfi  43534  sge0isum  43548  ovn02  43689
  Copyright terms: Public domain W3C validator