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

Theorem mpteq2da 4703
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 2621 . . 3 𝐴 = 𝐴
21ax-gen 1719 . 2 𝑥 𝐴 = 𝐴
3 mpteq2da.1 . . 3 𝑥𝜑
4 mpteq2da.2 . . . 4 ((𝜑𝑥𝐴) → 𝐵 = 𝐶)
54ex 450 . . 3 (𝜑 → (𝑥𝐴𝐵 = 𝐶))
63, 5ralrimi 2951 . 2 (𝜑 → ∀𝑥𝐴 𝐵 = 𝐶)
7 mpteq12f 4691 . 2 ((∀𝑥 𝐴 = 𝐴 ∧ ∀𝑥𝐴 𝐵 = 𝐶) → (𝑥𝐴𝐵) = (𝑥𝐴𝐶))
82, 6, 7sylancr 694 1 (𝜑 → (𝑥𝐴𝐵) = (𝑥𝐴𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  wal 1478   = wceq 1480  wnf 1705  wcel 1987  wral 2907  cmpt 4673
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-ral 2912  df-opab 4674  df-mpt 4675
This theorem is referenced by:  mpteq2dva  4704  offval2f  6862  prodeq1f  14563  prodeq2ii  14568  gsumsnfd  18272  gsummoncoe1  19593  cayleyhamilton1  20616  xkocnv  21527  utopsnneiplem  21961  fpwrelmap  29351  gsummpt2d  29566  esumf1o  29893  esum2d  29936  itg2addnclem  33093  ftc1anclem5  33121  mzpsubmpt  36786  mzpexpmpt  36788  refsum2cnlem1  38679  feqresmpt2  38936  fmuldfeqlem1  39218  limsupval3  39328  cncfiooicclem1  39410  dvmptfprodlem  39465  stoweidlem2  39526  stoweidlem6  39530  stoweidlem8  39532  stoweidlem17  39541  stoweidlem19  39543  stoweidlem20  39544  stoweidlem21  39545  stoweidlem22  39546  stoweidlem23  39547  stoweidlem32  39556  stoweidlem36  39560  stoweidlem40  39564  stoweidlem41  39565  stoweidlem47  39571  stirlinglem15  39612  sge0ss  39936  sge0xp  39953  omeiunlempt  40041  hoicvrrex  40077  ovnlecvr2  40131  smfdiv  40311  smfneg  40317  smflimmpt  40323  smfsupmpt  40328  smfinfmpt  40332  smflimsuplem4  40336  smflimsuplem5  40337  smflimsupmpt  40342
  Copyright terms: Public domain W3C validator