Theorem mpteq2da 5172

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1539  Ⅎwnf 1786   ∈ wcel 2106   ↦ cmpt 5157

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-12 2171  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-nf 1787  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-opab 5137  df-mpt 5158

This theorem is referenced by:  mpteq2dvaOLD  5175  offval2f  7548  prodeq1f  15618  prodeq2ii  15623  gsumsnfd  19552  gsummoncoe1  21475  cayleyhamilton1  22041  xkocnv  22965  utopsnneiplem  23399  fpwrelmap  31068  gsummpt2d  31309  elrspunidl  31606  fedgmullem2  31711  esumf1o  32018  esum2d  32061  itg2addnclem  35828  ftc1anclem5  35854  mzpsubmpt  40565  mzpexpmpt  40567  refsum2cnlem1  42580  fmuldfeqlem1  43123  limsupval3  43233  liminfval5  43306  liminfvalxrmpt  43327  liminfval4  43330  limsupval4  43335  liminfvaluz2  43336  limsupvaluz4  43341  cncfiooicclem1  43434  dvmptfprodlem  43485  stoweidlem2  43543  stoweidlem6  43547  stoweidlem8  43549  stoweidlem17  43558  stoweidlem19  43560  stoweidlem20  43561  stoweidlem21  43562  stoweidlem22  43563  stoweidlem23  43564  stoweidlem32  43573  stoweidlem36  43577  stoweidlem40  43581  stoweidlem41  43582  stoweidlem47  43588  stirlinglem15  43629  sge0ss  43950  sge0xp  43967  omeiunlempt  44058  hoicvrrex  44094  ovnlecvr2  44148  smfdiv  44331  smfneg  44337  smflimmpt  44343  smfsupmpt  44348  smfinfmpt  44352  smflimsuplem4  44356  smflimsuplem5  44357  smflimsupmpt  44362  smfliminf  44364  smfliminfmpt  44365