Theorem mpteq2da 5251

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

Syntax hints:   → wi 4   ∧ wa 394   = wceq 1534  Ⅎwnf 1778   ∈ wcel 2099   ↦ cmpt 5236

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-12 2167  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1775  df-nf 1779  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-opab 5216  df-mpt 5237

This theorem is referenced by:  mpteq2dvaOLD  5254  offval2f  7705  prodeq1f  15910  prodeq2ii  15915  gsumsnfd  19949  gsummoncoe1  22299  cayleyhamilton1  22885  xkocnv  23809  utopsnneiplem  24243  fpwrelmap  32647  gsummpt2d  32917  elrspunidl  33303  fedgmullem2  33525  esumf1o  33883  esum2d  33926  itg2addnclem  37372  ftc1anclem5  37398  mzpsubmpt  42400  mzpexpmpt  42402  refsum2cnlem1  44636  mpteq2dfa  44877  fmuldfeqlem1  45203  limsupval3  45313  liminfval5  45386  liminfvalxrmpt  45407  liminfval4  45410  limsupval4  45415  liminfvaluz2  45416  limsupvaluz4  45421  cncfiooicclem1  45514  dvmptfprodlem  45565  stoweidlem2  45623  stoweidlem6  45627  stoweidlem8  45629  stoweidlem17  45638  stoweidlem19  45640  stoweidlem20  45641  stoweidlem21  45642  stoweidlem22  45643  stoweidlem23  45644  stoweidlem32  45653  stoweidlem36  45657  stoweidlem40  45661  stoweidlem41  45662  stoweidlem47  45668  stirlinglem15  45709  sge0ss  46033  sge0xp  46050  omeiunlempt  46141  hoicvrrex  46177  ovnlecvr2  46231  smfdiv  46418  smfneg  46424  smflimmpt  46431  smfsupmpt  46436  smfinfmpt  46440  smflimsuplem4  46444  smflimsuplem5  46445  smflimsupmpt  46450  smfliminf  46452  smfliminfmpt  46453