Theorem mpteq2da 5124

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 2798	. . 3 ⊢ 𝐴 = 𝐴
2	1	ax-gen 1797	. 2 ⊢ ∀𝑥 𝐴 = 𝐴
3		mpteq2da.1	. . 3 ⊢ Ⅎ𝑥𝜑
4		mpteq2da.2	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)
5	4	ex 416	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝐵 = 𝐶))
6	3, 5	ralrimi 3180	. 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐵 = 𝐶)
7		mpteq12f 5113	. 2 ⊢ ((∀𝑥 𝐴 = 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝐵 = 𝐶) → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶))
8	2, 6, 7	sylancr 590	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶))

Syntax hints:   → wi 4   ∧ wa 399  ∀wal 1536   = wceq 1538  Ⅎwnf 1785   ∈ wcel 2111  ∀wral 3106   ↦ cmpt 5110

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-ral 3111  df-opab 5093  df-mpt 5111

This theorem is referenced by:  mpteq2dva  5125  offval2f  7401  prodeq1f  15254  prodeq2ii  15259  gsumsnfd  19064  gsummoncoe1  20933  cayleyhamilton1  21497  xkocnv  22419  utopsnneiplem  22853  fpwrelmap  30495  gsummpt2d  30734  elrspunidl  31014  fedgmullem2  31114  esumf1o  31419  esum2d  31462  itg2addnclem  35108  ftc1anclem5  35134  mzpsubmpt  39684  mzpexpmpt  39686  refsum2cnlem1  41666  fmuldfeqlem1  42224  limsupval3  42334  liminfval5  42407  liminfvalxrmpt  42428  liminfval4  42431  limsupval4  42436  liminfvaluz2  42437  limsupvaluz4  42442  cncfiooicclem1  42535  dvmptfprodlem  42586  stoweidlem2  42644  stoweidlem6  42648  stoweidlem8  42650  stoweidlem17  42659  stoweidlem19  42661  stoweidlem20  42662  stoweidlem21  42663  stoweidlem22  42664  stoweidlem23  42665  stoweidlem32  42674  stoweidlem36  42678  stoweidlem40  42682  stoweidlem41  42683  stoweidlem47  42689  stirlinglem15  42730  sge0ss  43051  sge0xp  43068  omeiunlempt  43159  hoicvrrex  43195  ovnlecvr2  43249  smfdiv  43429  smfneg  43435  smflimmpt  43441  smfsupmpt  43446  smfinfmpt  43450  smflimsuplem4  43454  smflimsuplem5  43455  smflimsupmpt  43460  smfliminf  43462  smfliminfmpt  43463