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

Theorem mpteq1 5145
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 2820 . . 3 (𝑥𝐴𝐶 = 𝐶)
21rgen 3146 . 2 𝑥𝐴 𝐶 = 𝐶
3 mpteq12 5144 . 2 ((𝐴 = 𝐵 ∧ ∀𝑥𝐴 𝐶 = 𝐶) → (𝑥𝐴𝐶) = (𝑥𝐵𝐶))
42, 3mpan2 689 1 (𝐴 = 𝐵 → (𝑥𝐴𝐶) = (𝑥𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1531  wcel 2108  wral 3136  cmpt 5137
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-12 2170  ax-ext 2791
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-clab 2798  df-cleq 2812  df-clel 2891  df-ral 3141  df-opab 5120  df-mpt 5138
This theorem is referenced by:  mpteq1d  5146  mpteq1i  5147  tposf12  7909  oarec  8180  wunex2  10152  wuncval2  10161  vrmdfval  18013  pmtrfval  18570  sylow1  18720  sylow2b  18740  sylow3lem5  18748  sylow3  18750  gsumconst  19046  gsum2dlem2  19083  mvrfval  20192  mplcoe1  20238  mplcoe5  20241  evlsval  20291  coe1fzgsumd  20462  evls1fval  20474  evl1gsumd  20512  gsumfsum  20604  mavmul0  21153  madugsum  21244  cramer0  21291  cnmpt1t  22265  cnmpt2t  22273  fmval  22543  symgtgp  22706  prdstgpd  22725  gsumvsca1  30847  gsumvsca2  30848  indv  31264  gsumesum  31311  esumlub  31312  esum2d  31345  sitg0  31597  matunitlindflem1  34880  matunitlindf  34882  sdclem2  35009  fsovcnvlem  40349  ntrneibex  40413  stoweidlem9  42284  sge0sn  42651  sge0iunmptlemfi  42685  sge0isum  42699  ovn02  42840
  Copyright terms: Public domain W3C validator