Theorem mpteq2da 5202

Description: Slightly more general equality inference for the maps-to notation. (Contributed by FL, 14-Sep-2013.) (Revised by Mario Carneiro, 16-Dec-2013.) (Proof shortened by SN, 11-Nov-2024.)

Hypotheses

Ref	Expression
mpteq2da.1	⊢ Ⅎ𝑥𝜑
mpteq2da.2	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)

Assertion

Ref	Expression
mpteq2da	⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶))

Proof of Theorem mpteq2da

Step	Hyp	Ref	Expression
1		mpteq2da.1	. 2 ⊢ Ⅎ𝑥𝜑
2		eqidd 2731	. 2 ⊢ (𝜑 → 𝐴 = 𝐴)
3		mpteq2da.2	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)
4	1, 2, 3	mpteq12da 5193	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶))

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540  Ⅎwnf 1783   ∈ wcel 2109   ↦ cmpt 5191

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-12 2178  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-opab 5173  df-mpt 5192

This theorem is referenced by:  offval2f  7671  prodeq1f  15879  prodeq2ii  15884  gsumsnfd  19888  gsummoncoe1  22202  cayleyhamilton1  22786  xkocnv  23708  utopsnneiplem  24142  itgeq1f  25679  fpwrelmap  32663  gsummpt2d  32996  elrgspnsubrunlem2  33206  elrspunidl  33406  fedgmullem2  33633  esumf1o  34047  esum2d  34090  itg2addnclem  37672  ftc1anclem5  37698  mzpsubmpt  42738  mzpexpmpt  42740  refsum2cnlem1  45038  mpteq2dfa  45268  fmuldfeqlem1  45587  limsupval3  45697  liminfval5  45770  liminfvalxrmpt  45791  liminfval4  45794  limsupval4  45799  liminfvaluz2  45800  limsupvaluz4  45805  cncfiooicclem1  45898  dvmptfprodlem  45949  stoweidlem2  46007  stoweidlem6  46011  stoweidlem8  46013  stoweidlem17  46022  stoweidlem19  46024  stoweidlem20  46025  stoweidlem21  46026  stoweidlem22  46027  stoweidlem23  46028  stoweidlem32  46037  stoweidlem36  46041  stoweidlem40  46045  stoweidlem41  46046  stoweidlem47  46052  stirlinglem15  46093  sge0ss  46417  sge0xp  46434  omeiunlempt  46525  hoicvrrex  46561  ovnlecvr2  46615  smfdiv  46802  smfneg  46808  smflimmpt  46815  smfsupmpt  46820  smfinfmpt  46824  smflimsuplem4  46828  smflimsuplem5  46829  smflimsupmpt  46834  smfliminf  46836  smfliminfmpt  46837