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

Theorem mpteq2da 4877
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 2771 . . 3 𝐴 = 𝐴
21ax-gen 1870 . 2 𝑥 𝐴 = 𝐴
3 mpteq2da.1 . . 3 𝑥𝜑
4 mpteq2da.2 . . . 4 ((𝜑𝑥𝐴) → 𝐵 = 𝐶)
54ex 397 . . 3 (𝜑 → (𝑥𝐴𝐵 = 𝐶))
63, 5ralrimi 3106 . 2 (𝜑 → ∀𝑥𝐴 𝐵 = 𝐶)
7 mpteq12f 4865 . 2 ((∀𝑥 𝐴 = 𝐴 ∧ ∀𝑥𝐴 𝐵 = 𝐶) → (𝑥𝐴𝐵) = (𝑥𝐴𝐶))
82, 6, 7sylancr 575 1 (𝜑 → (𝑥𝐴𝐵) = (𝑥𝐴𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  wal 1629   = wceq 1631  wnf 1856  wcel 2145  wral 3061  cmpt 4863
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-ral 3066  df-opab 4847  df-mpt 4864
This theorem is referenced by:  mpteq2dva  4878  offval2f  7056  prodeq1f  14845  prodeq2ii  14850  gsumsnfd  18558  gsummoncoe1  19889  cayleyhamilton1  20917  xkocnv  21838  utopsnneiplem  22271  fpwrelmap  29848  gsummpt2d  30121  esumf1o  30452  esum2d  30495  itg2addnclem  33793  ftc1anclem5  33821  mzpsubmpt  37832  mzpexpmpt  37834  refsum2cnlem1  39718  fmuldfeqlem1  40332  limsupval3  40442  liminfval5  40515  liminfvalxrmpt  40536  liminfval4  40539  limsupval4  40544  liminfvaluz2  40545  limsupvaluz4  40550  cncfiooicclem1  40624  dvmptfprodlem  40677  stoweidlem2  40736  stoweidlem6  40740  stoweidlem8  40742  stoweidlem17  40751  stoweidlem19  40753  stoweidlem20  40754  stoweidlem21  40755  stoweidlem22  40756  stoweidlem23  40757  stoweidlem32  40766  stoweidlem36  40770  stoweidlem40  40774  stoweidlem41  40775  stoweidlem47  40781  stirlinglem15  40822  sge0ss  41146  sge0xp  41163  omeiunlempt  41254  hoicvrrex  41290  ovnlecvr2  41344  smfdiv  41524  smfneg  41530  smflimmpt  41536  smfsupmpt  41541  smfinfmpt  41545  smflimsuplem4  41549  smflimsuplem5  41550  smflimsupmpt  41555  smfliminf  41557  smfliminfmpt  41558
  Copyright terms: Public domain W3C validator