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

Theorem mpteq2da 4734
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 2620 . . 3 𝐴 = 𝐴
21ax-gen 1720 . 2 𝑥 𝐴 = 𝐴
3 mpteq2da.1 . . 3 𝑥𝜑
4 mpteq2da.2 . . . 4 ((𝜑𝑥𝐴) → 𝐵 = 𝐶)
54ex 450 . . 3 (𝜑 → (𝑥𝐴𝐵 = 𝐶))
63, 5ralrimi 2954 . 2 (𝜑 → ∀𝑥𝐴 𝐵 = 𝐶)
7 mpteq12f 4722 . 2 ((∀𝑥 𝐴 = 𝐴 ∧ ∀𝑥𝐴 𝐵 = 𝐶) → (𝑥𝐴𝐵) = (𝑥𝐴𝐶))
82, 6, 7sylancr 694 1 (𝜑 → (𝑥𝐴𝐵) = (𝑥𝐴𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  wal 1479   = wceq 1481  wnf 1706  wcel 1988  wral 2909  cmpt 4720
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-ral 2914  df-opab 4704  df-mpt 4721
This theorem is referenced by:  mpteq2dva  4735  offval2f  6894  prodeq1f  14619  prodeq2ii  14624  gsumsnfd  18332  gsummoncoe1  19655  cayleyhamilton1  20678  xkocnv  21598  utopsnneiplem  22032  fpwrelmap  29482  gsummpt2d  29755  esumf1o  30086  esum2d  30129  itg2addnclem  33432  ftc1anclem5  33460  mzpsubmpt  37125  mzpexpmpt  37127  refsum2cnlem1  39016  fmuldfeqlem1  39614  limsupval3  39724  liminfval5  39791  liminfvalxrmpt  39812  liminfval4  39815  limsupval4  39820  liminfvaluz2  39821  limsupvaluz4  39826  cncfiooicclem1  39869  dvmptfprodlem  39922  stoweidlem2  39982  stoweidlem6  39986  stoweidlem8  39988  stoweidlem17  39997  stoweidlem19  39999  stoweidlem20  40000  stoweidlem21  40001  stoweidlem22  40002  stoweidlem23  40003  stoweidlem32  40012  stoweidlem36  40016  stoweidlem40  40020  stoweidlem41  40021  stoweidlem47  40027  stirlinglem15  40068  sge0ss  40392  sge0xp  40409  omeiunlempt  40497  hoicvrrex  40533  ovnlecvr2  40587  smfdiv  40767  smfneg  40773  smflimmpt  40779  smfsupmpt  40784  smfinfmpt  40788  smflimsuplem4  40792  smflimsuplem5  40793  smflimsupmpt  40798  smfliminf  40800  smfliminfmpt  40801
  Copyright terms: Public domain W3C validator