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

Theorem mpteq12dva 5136
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 1929 . 2 (𝜑 → ∀𝑥 𝐴 = 𝐶)
3 mpteq12dva.2 . . 3 ((𝜑𝑥𝐴) → 𝐵 = 𝐷)
43ralrimiva 3177 . 2 (𝜑 → ∀𝑥𝐴 𝐵 = 𝐷)
5 mpteq12f 5135 . 2 ((∀𝑥 𝐴 = 𝐶 ∧ ∀𝑥𝐴 𝐵 = 𝐷) → (𝑥𝐴𝐵) = (𝑥𝐶𝐷))
62, 4, 5syl2anc 587 1 (𝜑 → (𝑥𝐴𝐵) = (𝑥𝐶𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  wal 1536   = wceq 1538  wcel 2115  wral 3133  cmpt 5132
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 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-12 2179  ax-ext 2796
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 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-ral 3138  df-opab 5115  df-mpt 5133
This theorem is referenced by:  mpteq12dvOLD  5138  pfxmpt  14040  reps  14132  repswccat  14148  cidpropd  16980  monpropd  17007  fucpropd  17247  curfpropd  17483  hofpropd  17517  yonffthlem  17532  ofco2  21063  pmatcollpw3fi1lem1  21397  rrxnm  24001  ushgredgedg  27025  ushgredgedgloop  27027  cshw1s2  30648  cycpm2tr  30796  sgnsv  30837  extdg1id  31116  ofcfval  31417  ccatmulgnn0dir  31872  signstf0  31898  curunc  34987  cncfiooicc  42466  dvcosax  42498  fourierdlem74  42752  fourierdlem75  42753  fourierdlem93  42771  smfsupxr  43377  smflimsuplem8  43388
  Copyright terms: Public domain W3C validator