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

Theorem mpteq12 4870
Description: An equality theorem for the maps to notation. (Contributed by NM, 16-Dec-2013.)
Assertion
Ref Expression
mpteq12 ((𝐴 = 𝐶 ∧ ∀𝑥𝐴 𝐵 = 𝐷) → (𝑥𝐴𝐵) = (𝑥𝐶𝐷))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐶
Allowed substitution hints:   𝐵(𝑥)   𝐷(𝑥)

Proof of Theorem mpteq12
StepHypRef Expression
1 ax-5 1991 . 2 (𝐴 = 𝐶 → ∀𝑥 𝐴 = 𝐶)
2 mpteq12f 4865 . 2 ((∀𝑥 𝐴 = 𝐶 ∧ ∀𝑥𝐴 𝐵 = 𝐷) → (𝑥𝐴𝐵) = (𝑥𝐶𝐷))
31, 2sylan 569 1 ((𝐴 = 𝐶 ∧ ∀𝑥𝐴 𝐵 = 𝐷) → (𝑥𝐴𝐵) = (𝑥𝐶𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  wal 1629   = wceq 1631  wral 3061  cmpt 4863
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-ral 3066  df-opab 4847  df-mpt 4864
This theorem is referenced by:  mpteq1  4871  mpteqb  6441  fmptcof  6540  mapxpen  8282  prodeq2w  14849  prdsdsval2  16352  prdsdsval3  16353  ablfac2  18696  mdetunilem9  20644  mdetmul  20647  xkocnv  21838  voliun  23542  itgeq1f  23758  itgeq2  23764  iblcnlem  23775  esumeq2  30438  esumcvg  30488  dvtan  33792  bddiblnc  33812
  Copyright terms: Public domain W3C validator