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

Theorem mpteq12 5120
 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 1911 . 2 (𝐴 = 𝐶 → ∀𝑥 𝐴 = 𝐶)
2 mpteq12f 5116 . 2 ((∀𝑥 𝐴 = 𝐶 ∧ ∀𝑥𝐴 𝐵 = 𝐷) → (𝑥𝐴𝐵) = (𝑥𝐶𝐷))
31, 2sylan 583 1 ((𝐴 = 𝐶 ∧ ∀𝑥𝐴 𝐵 = 𝐷) → (𝑥𝐴𝐵) = (𝑥𝐶𝐷))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399  ∀wal 1536   = wceq 1538  ∀wral 3109   ↦ cmpt 5113 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-12 2176  ax-ext 2773 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-ral 3114  df-opab 5096  df-mpt 5114 This theorem is referenced by:  mpteq1  5121  mpteqb  6768  fmptcof  6873  mapxpen  8671  prodeq2w  15262  prdsdsval2  16753  prdsdsval3  16754  ablfac2  19208  mdetunilem9  21229  mdetmul  21232  xkocnv  22423  voliun  24162  itgeq1f  24379  itgeq2  24385  iblcnlem  24396  bddiblnc  24449  esumeq2  31409  esumcvg  31459  dvtan  35106
 Copyright terms: Public domain W3C validator