Theorem mpteq2da 5190

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 2737	. 2 ⊢ (𝜑 → 𝐴 = 𝐴)
3		mpteq2da.2	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)
4	1, 2, 3	mpteq12da 5181	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶))

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541  Ⅎwnf 1784   ∈ wcel 2113   ↦ cmpt 5179

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-12 2184  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-nf 1785  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-opab 5161  df-mpt 5180

This theorem is referenced by:  offval2f  7637  prodeq1f  15829  prodeq2ii  15834  gsumsnfd  19880  gsummoncoe1  22252  cayleyhamilton1  22836  xkocnv  23758  utopsnneiplem  24191  itgeq1f  25728  fpwrelmap  32812  gsummpt2d  33132  elrgspnsubrunlem2  33330  elrspunidl  33509  fedgmullem2  33787  esumf1o  34207  esum2d  34250  itg2addnclem  37868  ftc1anclem5  37894  mzpsubmpt  42981  mzpexpmpt  42983  refsum2cnlem1  45278  mpteq2dfa  45507  fmuldfeqlem1  45824  limsupval3  45932  liminfval5  46005  liminfvalxrmpt  46026  liminfval4  46029  limsupval4  46034  liminfvaluz2  46035  limsupvaluz4  46040  cncfiooicclem1  46133  dvmptfprodlem  46184  stoweidlem2  46242  stoweidlem6  46246  stoweidlem8  46248  stoweidlem17  46257  stoweidlem19  46259  stoweidlem20  46260  stoweidlem21  46261  stoweidlem22  46262  stoweidlem23  46263  stoweidlem32  46272  stoweidlem36  46276  stoweidlem40  46280  stoweidlem41  46281  stoweidlem47  46287  stirlinglem15  46328  sge0ss  46652  sge0xp  46669  omeiunlempt  46760  hoicvrrex  46796  ovnlecvr2  46850  smfdiv  47037  smfneg  47043  smflimmpt  47050  smfsupmpt  47055  smfinfmpt  47059  smflimsuplem4  47063  smflimsuplem5  47064  smflimsupmpt  47069  smfliminf  47071  smfliminfmpt  47072