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

Theorem mpteq12dva 4692
 Description: An equality inference for the maps to notation. (Contributed by Mario Carneiro, 26-Jan-2017.)
Hypotheses
Ref Expression
mpteq12dv.1 (𝜑𝐴 = 𝐶)
mpteq12dva.2 ((𝜑𝑥𝐴) → 𝐵 = 𝐷)
Assertion
Ref Expression
mpteq12dva (𝜑 → (𝑥𝐴𝐵) = (𝑥𝐶𝐷))
Distinct variable group:   𝜑,𝑥
Allowed substitution hints:   𝐴(𝑥)   𝐵(𝑥)   𝐶(𝑥)   𝐷(𝑥)

Proof of Theorem mpteq12dva
StepHypRef Expression
1 mpteq12dv.1 . . 3 (𝜑𝐴 = 𝐶)
21alrimiv 1852 . 2 (𝜑 → ∀𝑥 𝐴 = 𝐶)
3 mpteq12dva.2 . . 3 ((𝜑𝑥𝐴) → 𝐵 = 𝐷)
43ralrimiva 2960 . 2 (𝜑 → ∀𝑥𝐴 𝐵 = 𝐷)
5 mpteq12f 4691 . 2 ((∀𝑥 𝐴 = 𝐶 ∧ ∀𝑥𝐴 𝐵 = 𝐷) → (𝑥𝐴𝐵) = (𝑥𝐶𝐷))
62, 4, 5syl2anc 692 1 (𝜑 → (𝑥𝐴𝐵) = (𝑥𝐶𝐷))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 384  ∀wal 1478   = wceq 1480   ∈ wcel 1987  ∀wral 2907   ↦ cmpt 4673 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-ral 2912  df-opab 4674  df-mpt 4675 This theorem is referenced by:  mpteq12dv  4693  reps  13454  repswccat  13469  cidpropd  16291  monpropd  16318  fucpropd  16558  curfpropd  16794  hofpropd  16828  yonffthlem  16843  ofco2  20176  pmatcollpw3fi1lem1  20510  rrxnm  23087  ushgredgedg  26014  ushgredgedgloop  26016  sgnsv  29512  ofcfval  29941  ccatmulgnn0dir  30399  signstf0  30425  curunc  33023  cncfiooicc  39411  dvcosax  39447  fourierdlem74  39704  fourierdlem75  39705  fourierdlem93  39723  smfsupxr  40329  smflimsuplem8  40340  pfxmpt  40686
 Copyright terms: Public domain W3C validator