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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1570  Ⅎwnf 1813   ∈ wcel 2143   ↦ cmpt 5193

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-12 2213  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-nf 1814  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-opab 5175  df-mpt 5194

This theorem is referenced by:  offval2f  7691  prodeq1f  15962  prodeq2ii  15967  gsumsnfd  20022  gsummoncoe1  22449  cayleyhamilton1  23030  xkocnv  23952  utopsnneiplem  24385  itgeq1f  25911  fpwrelmap  33056  gsummpt2d  33347  suppgsumssiun  33370  elrgspnsubrunlem2  33546  elrspunidl  33714  fedgmullem2  33998  esumf1o  34418  esum2d  34461  itg2addnclem  38300  ftc1anclem5  38326  mzpsubmpt  43454  mzpexpmpt  43456  refsum2cnlem1  45737  mpteq2dfa  45962  fmuldfeqlem1  46278  limsupval3  46386  liminfval5  46459  liminfvalxrmpt  46480  liminfval4  46483  limsupval4  46488  liminfvaluz2  46489  limsupvaluz4  46494  cncfiooicclem1  46587  dvmptfprodlem  46638  stoweidlem2  46696  stoweidlem6  46700  stoweidlem8  46702  stoweidlem17  46711  stoweidlem19  46713  stoweidlem20  46714  stoweidlem21  46715  stoweidlem22  46716  stoweidlem23  46717  stoweidlem32  46726  stoweidlem36  46730  stoweidlem40  46734  stoweidlem41  46735  stoweidlem47  46741  stirlinglem15  46782  sge0ss  47106  sge0xp  47123  omeiunlempt  47214  hoicvrrex  47250  ovnlecvr2  47304  smfdiv  47491  smfneg  47497  smflimmpt  47504  smfsupmpt  47509  smfinfmpt  47513  smflimsuplem4  47517  smflimsuplem5  47518  smflimsupmpt  47523  smfliminf  47525  smfliminfmpt  47526