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

Theorem mpteq2da 5246
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 2732 . 2 (𝜑𝐴 = 𝐴)
3 mpteq2da.2 . 2 ((𝜑𝑥𝐴) → 𝐵 = 𝐶)
41, 2, 3mpteq12da 5233 1 (𝜑 → (𝑥𝐴𝐵) = (𝑥𝐴𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395   = wceq 1540  wnf 1784  wcel 2105  cmpt 5231
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-12 2170  ax-ext 2702
This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1781  df-nf 1785  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-opab 5211  df-mpt 5232
This theorem is referenced by:  mpteq2dvaOLD  5249  offval2f  7688  prodeq1f  15857  prodeq2ii  15862  gsumsnfd  19861  gsummoncoe1  22049  cayleyhamilton1  22615  xkocnv  23539  utopsnneiplem  23973  fpwrelmap  32226  gsummpt2d  32472  elrspunidl  32821  fedgmullem2  33004  esumf1o  33347  esum2d  33390  itg2addnclem  36843  ftc1anclem5  36869  mzpsubmpt  41784  mzpexpmpt  41786  refsum2cnlem1  44024  mpteq2dfa  44271  fmuldfeqlem1  44597  limsupval3  44707  liminfval5  44780  liminfvalxrmpt  44801  liminfval4  44804  limsupval4  44809  liminfvaluz2  44810  limsupvaluz4  44815  cncfiooicclem1  44908  dvmptfprodlem  44959  stoweidlem2  45017  stoweidlem6  45021  stoweidlem8  45023  stoweidlem17  45032  stoweidlem19  45034  stoweidlem20  45035  stoweidlem21  45036  stoweidlem22  45037  stoweidlem23  45038  stoweidlem32  45047  stoweidlem36  45051  stoweidlem40  45055  stoweidlem41  45056  stoweidlem47  45062  stirlinglem15  45103  sge0ss  45427  sge0xp  45444  omeiunlempt  45535  hoicvrrex  45571  ovnlecvr2  45625  smfdiv  45812  smfneg  45818  smflimmpt  45825  smfsupmpt  45830  smfinfmpt  45834  smflimsuplem4  45838  smflimsuplem5  45839  smflimsupmpt  45844  smfliminf  45846  smfliminfmpt  45847
  Copyright terms: Public domain W3C validator