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

Theorem mpteq12i 4775
 Description: An equality inference for the maps to notation. (Contributed by Scott Fenton, 27-Oct-2010.) (Revised by Mario Carneiro, 16-Dec-2013.)
Hypotheses
Ref Expression
mpteq12i.1 𝐴 = 𝐶
mpteq12i.2 𝐵 = 𝐷
Assertion
Ref Expression
mpteq12i (𝑥𝐴𝐵) = (𝑥𝐶𝐷)

Proof of Theorem mpteq12i
StepHypRef Expression
1 mpteq12i.1 . . . 4 𝐴 = 𝐶
21a1i 11 . . 3 (⊤ → 𝐴 = 𝐶)
3 mpteq12i.2 . . . 4 𝐵 = 𝐷
43a1i 11 . . 3 (⊤ → 𝐵 = 𝐷)
52, 4mpteq12dv 4766 . 2 (⊤ → (𝑥𝐴𝐵) = (𝑥𝐶𝐷))
65trud 1533 1 (𝑥𝐴𝐵) = (𝑥𝐶𝐷)
 Colors of variables: wff setvar class Syntax hints:   = wceq 1523  ⊤wtru 1524   ↦ cmpt 4762 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-ral 2946  df-opab 4746  df-mpt 4763 This theorem is referenced by:  offres  7205  pmtrprfval  17953  evlsval  19567  madufval  20491  limcdif  23685  dfhnorm2  28107  cdj3lem3  29425  cdj3lem3b  29427  partfun  29603  esumsnf  30254  esumrnmpt2  30258  measinb2  30414  eulerpart  30572  fiblem  30588  trlset  35766  hoidmvlelem4  41133  smflimsup  41355
 Copyright terms: Public domain W3C validator