Theorem mpteq2da 5177

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 5168	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶))

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542  Ⅎwnf 1785   ∈ wcel 2114   ↦ cmpt 5166

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-12 2185  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-nf 1786  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-opab 5148  df-mpt 5167

This theorem is referenced by:  offval2f  7646  prodeq1f  15871  prodeq2ii  15876  gsumsnfd  19926  gsummoncoe1  22273  cayleyhamilton1  22857  xkocnv  23779  utopsnneiplem  24212  itgeq1f  25738  fpwrelmap  32806  gsummpt2d  33110  suppgsumssiun  33133  elrgspnsubrunlem2  33309  elrspunidl  33488  fedgmullem2  33774  esumf1o  34194  esum2d  34237  itg2addnclem  37992  ftc1anclem5  38018  mzpsubmpt  43175  mzpexpmpt  43177  refsum2cnlem1  45468  mpteq2dfa  45696  fmuldfeqlem1  46012  limsupval3  46120  liminfval5  46193  liminfvalxrmpt  46214  liminfval4  46217  limsupval4  46222  liminfvaluz2  46223  limsupvaluz4  46228  cncfiooicclem1  46321  dvmptfprodlem  46372  stoweidlem2  46430  stoweidlem6  46434  stoweidlem8  46436  stoweidlem17  46445  stoweidlem19  46447  stoweidlem20  46448  stoweidlem21  46449  stoweidlem22  46450  stoweidlem23  46451  stoweidlem32  46460  stoweidlem36  46464  stoweidlem40  46468  stoweidlem41  46469  stoweidlem47  46475  stirlinglem15  46516  sge0ss  46840  sge0xp  46857  omeiunlempt  46948  hoicvrrex  46984  ovnlecvr2  47038  smfdiv  47225  smfneg  47231  smflimmpt  47238  smfsupmpt  47243  smfinfmpt  47247  smflimsuplem4  47251  smflimsuplem5  47252  smflimsupmpt  47257  smfliminf  47259  smfliminfmpt  47260