Theorem mpteq2da 5191

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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1559  Ⅎwnf 1802   ∈ wcel 2141   ↦ cmpt 5180

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-12 2211  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-nf 1803  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-opab 5162  df-mpt 5181

This theorem is referenced by:  offval2f  7671  prodeq1f  15919  prodeq2ii  15924  gsumsnfd  19974  gsummoncoe1  22351  cayleyhamilton1  22932  xkocnv  23854  utopsnneiplem  24287  itgeq1f  25813  fpwrelmap  32885  gsummpt2d  33190  suppgsumssiun  33213  elrgspnsubrunlem2  33390  elrspunidl  33575  fedgmullem2  33888  esumf1o  34308  esum2d  34351  itg2addnclem  38134  ftc1anclem5  38160  mzpsubmpt  43288  mzpexpmpt  43290  refsum2cnlem1  45581  mpteq2dfa  45806  fmuldfeqlem1  46122  limsupval3  46230  liminfval5  46303  liminfvalxrmpt  46324  liminfval4  46327  limsupval4  46332  liminfvaluz2  46333  limsupvaluz4  46338  cncfiooicclem1  46431  dvmptfprodlem  46482  stoweidlem2  46540  stoweidlem6  46544  stoweidlem8  46546  stoweidlem17  46555  stoweidlem19  46557  stoweidlem20  46558  stoweidlem21  46559  stoweidlem22  46560  stoweidlem23  46561  stoweidlem32  46570  stoweidlem36  46574  stoweidlem40  46578  stoweidlem41  46579  stoweidlem47  46585  stirlinglem15  46626  sge0ss  46950  sge0xp  46967  omeiunlempt  47058  hoicvrrex  47094  ovnlecvr2  47148  smfdiv  47335  smfneg  47341  smflimmpt  47348  smfsupmpt  47353  smfinfmpt  47357  smflimsuplem4  47361  smflimsuplem5  47362  smflimsupmpt  47367  smfliminf  47369  smfliminfmpt  47370