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

Theorem mpteq2da 4671
 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 2610 . . 3 𝐴 = 𝐴
21ax-gen 1713 . 2 𝑥 𝐴 = 𝐴
3 mpteq2da.1 . . 3 𝑥𝜑
4 mpteq2da.2 . . . 4 ((𝜑𝑥𝐴) → 𝐵 = 𝐶)
54ex 449 . . 3 (𝜑 → (𝑥𝐴𝐵 = 𝐶))
63, 5ralrimi 2940 . 2 (𝜑 → ∀𝑥𝐴 𝐵 = 𝐶)
7 mpteq12f 4661 . 2 ((∀𝑥 𝐴 = 𝐴 ∧ ∀𝑥𝐴 𝐵 = 𝐶) → (𝑥𝐴𝐵) = (𝑥𝐴𝐶))
82, 6, 7sylancr 694 1 (𝜑 → (𝑥𝐴𝐵) = (𝑥𝐴𝐶))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383  ∀wal 1473   = wceq 1475  Ⅎwnf 1699   ∈ 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:  mpteq2dva  4672  offval2f  6807  prodeq1f  14477  prodeq2ii  14482  gsumsnfd  18174  gsummoncoe1  19495  cayleyhamilton1  20516  xkocnv  21427  utopsnneiplem  21861  fpwrelmap  28896  gsummpt2d  29112  esumf1o  29439  esum2d  29482  itg2addnclem  32631  ftc1anclem5  32659  mzpsubmpt  36324  mzpexpmpt  36326  refsum2cnlem1  38219  fmuldfeqlem1  38649  cncfiooicclem1  38779  dvmptfprodlem  38834  stoweidlem2  38895  stoweidlem6  38899  stoweidlem8  38901  stoweidlem17  38910  stoweidlem19  38912  stoweidlem20  38913  stoweidlem21  38914  stoweidlem22  38915  stoweidlem23  38916  stoweidlem32  38925  stoweidlem36  38929  stoweidlem40  38933  stoweidlem41  38934  stoweidlem47  38940  stirlinglem15  38981  sge0ss  39305  sge0xp  39322  omeiunlempt  39410  hoicvrrex  39446  ovnlecvr2  39500  smfdiv  39682
 Copyright terms: Public domain W3C validator