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

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

Proof of Theorem mpteq2da
StepHypRef Expression
1 mpteq2da.1 . 2 𝑥𝜑
2 eqidd 2738 . 2 (𝜑𝐴 = 𝐴)
3 mpteq2da.2 . 2 ((𝜑𝑥𝐴) → 𝐵 = 𝐶)
41, 2, 3mpteq12da 5191 1 (𝜑 → (𝑥𝐴𝐵) = (𝑥𝐴𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397   = wceq 1542  wnf 1786  wcel 2107  cmpt 5189
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-12 2172  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-opab 5169  df-mpt 5190
This theorem is referenced by:  mpteq2dvaOLD  5207  offval2f  7633  prodeq1f  15792  prodeq2ii  15797  gsumsnfd  19729  gsummoncoe1  21678  cayleyhamilton1  22244  xkocnv  23168  utopsnneiplem  23602  fpwrelmap  31653  gsummpt2d  31894  elrspunidl  32206  fedgmullem2  32328  esumf1o  32652  esum2d  32695  itg2addnclem  36132  ftc1anclem5  36158  mzpsubmpt  41069  mzpexpmpt  41071  refsum2cnlem1  43249  mpteq2dfa  43503  fmuldfeqlem1  43830  limsupval3  43940  liminfval5  44013  liminfvalxrmpt  44034  liminfval4  44037  limsupval4  44042  liminfvaluz2  44043  limsupvaluz4  44048  cncfiooicclem1  44141  dvmptfprodlem  44192  stoweidlem2  44250  stoweidlem6  44254  stoweidlem8  44256  stoweidlem17  44265  stoweidlem19  44267  stoweidlem20  44268  stoweidlem21  44269  stoweidlem22  44270  stoweidlem23  44271  stoweidlem32  44280  stoweidlem36  44284  stoweidlem40  44288  stoweidlem41  44289  stoweidlem47  44295  stirlinglem15  44336  sge0ss  44660  sge0xp  44677  omeiunlempt  44768  hoicvrrex  44804  ovnlecvr2  44858  smfdiv  45045  smfneg  45051  smflimmpt  45058  smfsupmpt  45063  smfinfmpt  45067  smflimsuplem4  45071  smflimsuplem5  45072  smflimsupmpt  45077  smfliminf  45079  smfliminfmpt  45080
  Copyright terms: Public domain W3C validator