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

Theorem mpteq12dva 4662
 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 1842 . 2 (𝜑 → ∀𝑥 𝐴 = 𝐶)
3 mpteq12dva.2 . . 3 ((𝜑𝑥𝐴) → 𝐵 = 𝐷)
43ralrimiva 2949 . 2 (𝜑 → ∀𝑥𝐴 𝐵 = 𝐷)
5 mpteq12f 4661 . 2 ((∀𝑥 𝐴 = 𝐶 ∧ ∀𝑥𝐴 𝐵 = 𝐷) → (𝑥𝐴𝐵) = (𝑥𝐶𝐷))
62, 4, 5syl2anc 691 1 (𝜑 → (𝑥𝐴𝐵) = (𝑥𝐶𝐷))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383  ∀wal 1473   = wceq 1475   ∈ wcel 1977  ∀wral 2896   ↦ cmpt 4643 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-ral 2901  df-opab 4644  df-mpt 4645 This theorem is referenced by:  mpteq12dv  4663  reps  13368  repswccat  13383  cidpropd  16193  monpropd  16220  fucpropd  16460  curfpropd  16696  hofpropd  16730  yonffthlem  16745  ofco2  20076  pmatcollpw3fi1lem1  20410  rrxnm  22987  sgnsv  29058  ofcfval  29487  ccatmulgnn0dir  29945  signstf0  29971  curunc  32561  cncfiooicc  38780  dvcosax  38816  fourierdlem74  39073  fourierdlem75  39074  fourierdlem93  39092  pfxmpt  40250  ushgredgedga  40456  ushgredgedgaloop  40458
 Copyright terms: Public domain W3C validator