Theorem mpteq2da 5204

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1567  Ⅎwnf 1810   ∈ wcel 2149   ↦ cmpt 5193

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-12 2219  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-nf 1811  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-opab 5175  df-mpt 5194

This theorem is referenced by:  offval2f  7687  prodeq1f  15956  prodeq2ii  15961  gsumsnfd  20017  gsummoncoe1  22433  cayleyhamilton1  23014  xkocnv  23936  utopsnneiplem  24369  itgeq1f  25895  fpwrelmap  33015  gsummpt2d  33306  suppgsumssiun  33329  elrgspnsubrunlem2  33505  elrspunidl  33676  fedgmullem2  33961  esumf1o  34381  esum2d  34424  itg2addnclem  38205  ftc1anclem5  38231  mzpsubmpt  43359  mzpexpmpt  43361  refsum2cnlem1  45642  mpteq2dfa  45867  fmuldfeqlem1  46183  limsupval3  46291  liminfval5  46364  liminfvalxrmpt  46385  liminfval4  46388  limsupval4  46393  liminfvaluz2  46394  limsupvaluz4  46399  cncfiooicclem1  46492  dvmptfprodlem  46543  stoweidlem2  46601  stoweidlem6  46605  stoweidlem8  46607  stoweidlem17  46616  stoweidlem19  46618  stoweidlem20  46619  stoweidlem21  46620  stoweidlem22  46621  stoweidlem23  46622  stoweidlem32  46631  stoweidlem36  46635  stoweidlem40  46639  stoweidlem41  46640  stoweidlem47  46646  stirlinglem15  46687  sge0ss  47011  sge0xp  47028  omeiunlempt  47119  hoicvrrex  47155  ovnlecvr2  47209  smfdiv  47396  smfneg  47402  smflimmpt  47409  smfsupmpt  47414  smfinfmpt  47418  smflimsuplem4  47422  smflimsuplem5  47423  smflimsupmpt  47428  smfliminf  47430  smfliminfmpt  47431