Theorem mpteq2da 4743

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

Step	Hyp	Ref	Expression
1		eqid 2622	. . 3 ⊢ 𝐴 = 𝐴
2	1	ax-gen 1722	. 2 ⊢ ∀𝑥 𝐴 = 𝐴
3		mpteq2da.1	. . 3 ⊢ Ⅎ𝑥𝜑
4		mpteq2da.2	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)
5	4	ex 450	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝐵 = 𝐶))
6	3, 5	ralrimi 2957	. 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐵 = 𝐶)
7		mpteq12f 4731	. 2 ⊢ ((∀𝑥 𝐴 = 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝐵 = 𝐶) → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶))
8	2, 6, 7	sylancr 695	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶))

Syntax hints:   → wi 4   ∧ wa 384  ∀wal 1481   = wceq 1483  Ⅎwnf 1708   ∈ wcel 1990  ∀wral 2912   ↦ cmpt 4729

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-ral 2917  df-opab 4713  df-mpt 4730

This theorem is referenced by:  mpteq2dva  4744  offval2f  6909  prodeq1f  14638  prodeq2ii  14643  gsumsnfd  18351  gsummoncoe1  19674  cayleyhamilton1  20697  xkocnv  21617  utopsnneiplem  22051  fpwrelmap  29508  gsummpt2d  29781  esumf1o  30112  esum2d  30155  itg2addnclem  33461  ftc1anclem5  33489  mzpsubmpt  37306  mzpexpmpt  37308  refsum2cnlem1  39196  fmuldfeqlem1  39814  limsupval3  39924  liminfval5  39997  liminfvalxrmpt  40018  liminfval4  40021  limsupval4  40026  liminfvaluz2  40027  limsupvaluz4  40032  cncfiooicclem1  40106  dvmptfprodlem  40159  stoweidlem2  40219  stoweidlem6  40223  stoweidlem8  40225  stoweidlem17  40234  stoweidlem19  40236  stoweidlem20  40237  stoweidlem21  40238  stoweidlem22  40239  stoweidlem23  40240  stoweidlem32  40249  stoweidlem36  40253  stoweidlem40  40257  stoweidlem41  40258  stoweidlem47  40264  stirlinglem15  40305  sge0ss  40629  sge0xp  40646  omeiunlempt  40734  hoicvrrex  40770  ovnlecvr2  40824  smfdiv  41004  smfneg  41010  smflimmpt  41016  smfsupmpt  41021  smfinfmpt  41025  smflimsuplem4  41029  smflimsuplem5  41030  smflimsupmpt  41035  smfliminf  41037  smfliminfmpt  41038