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

Theorem mpteq2da 5151
Description: Slightly more general equality inference for the maps-to notation. (Contributed by FL, 14-Sep-2013.) (Revised by Mario Carneiro, 16-Dec-2013.)
Hypotheses
Ref Expression
mpteq2da.1 𝑥𝜑
mpteq2da.2 ((𝜑𝑥𝐴) → 𝐵 = 𝐶)
Assertion
Ref Expression
mpteq2da (𝜑 → (𝑥𝐴𝐵) = (𝑥𝐴𝐶))

Proof of Theorem mpteq2da
StepHypRef Expression
1 eqid 2819 . . 3 𝐴 = 𝐴
21ax-gen 1790 . 2 𝑥 𝐴 = 𝐴
3 mpteq2da.1 . . 3 𝑥𝜑
4 mpteq2da.2 . . . 4 ((𝜑𝑥𝐴) → 𝐵 = 𝐶)
54ex 415 . . 3 (𝜑 → (𝑥𝐴𝐵 = 𝐶))
63, 5ralrimi 3214 . 2 (𝜑 → ∀𝑥𝐴 𝐵 = 𝐶)
7 mpteq12f 5140 . 2 ((∀𝑥 𝐴 = 𝐴 ∧ ∀𝑥𝐴 𝐵 = 𝐶) → (𝑥𝐴𝐵) = (𝑥𝐴𝐶))
82, 6, 7sylancr 589 1 (𝜑 → (𝑥𝐴𝐵) = (𝑥𝐴𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 398  wal 1529   = wceq 1531  wnf 1778  wcel 2108  wral 3136  cmpt 5137
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-12 2170  ax-ext 2791
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-clab 2798  df-cleq 2812  df-clel 2891  df-ral 3141  df-opab 5120  df-mpt 5138
This theorem is referenced by:  mpteq2dva  5152  offval2f  7413  prodeq1f  15254  prodeq2ii  15259  gsumsnfd  19063  gsummoncoe1  20464  cayleyhamilton1  21492  xkocnv  22414  utopsnneiplem  22848  fpwrelmap  30461  gsummpt2d  30680  fedgmullem2  31019  esumf1o  31302  esum2d  31345  itg2addnclem  34935  ftc1anclem5  34963  mzpsubmpt  39331  mzpexpmpt  39333  refsum2cnlem1  41285  fmuldfeqlem1  41853  limsupval3  41963  liminfval5  42036  liminfvalxrmpt  42057  liminfval4  42060  limsupval4  42065  liminfvaluz2  42066  limsupvaluz4  42071  cncfiooicclem1  42166  dvmptfprodlem  42219  stoweidlem2  42278  stoweidlem6  42282  stoweidlem8  42284  stoweidlem17  42293  stoweidlem19  42295  stoweidlem20  42296  stoweidlem21  42297  stoweidlem22  42298  stoweidlem23  42299  stoweidlem32  42308  stoweidlem36  42312  stoweidlem40  42316  stoweidlem41  42317  stoweidlem47  42323  stirlinglem15  42364  sge0ss  42685  sge0xp  42702  omeiunlempt  42793  hoicvrrex  42829  ovnlecvr2  42883  smfdiv  43063  smfneg  43069  smflimmpt  43075  smfsupmpt  43080  smfinfmpt  43084  smflimsuplem4  43088  smflimsuplem5  43089  smflimsupmpt  43094  smfliminf  43096  smfliminfmpt  43097
  Copyright terms: Public domain W3C validator