Theorem mpteq2da 5264

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1537  Ⅎwnf 1781   ∈ wcel 2108   ↦ cmpt 5249

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-12 2178  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-nf 1782  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-opab 5229  df-mpt 5250

This theorem is referenced by:  mpteq2dvaOLD  5267  offval2f  7729  prodeq1f  15954  prodeq2ii  15959  gsumsnfd  19993  gsummoncoe1  22333  cayleyhamilton1  22919  xkocnv  23843  utopsnneiplem  24277  itgeq1f  25826  fpwrelmap  32747  gsummpt2d  33032  elrspunidl  33421  fedgmullem2  33643  esumf1o  34014  esum2d  34057  itg2addnclem  37631  ftc1anclem5  37657  mzpsubmpt  42699  mzpexpmpt  42701  refsum2cnlem1  44937  mpteq2dfa  45177  fmuldfeqlem1  45503  limsupval3  45613  liminfval5  45686  liminfvalxrmpt  45707  liminfval4  45710  limsupval4  45715  liminfvaluz2  45716  limsupvaluz4  45721  cncfiooicclem1  45814  dvmptfprodlem  45865  stoweidlem2  45923  stoweidlem6  45927  stoweidlem8  45929  stoweidlem17  45938  stoweidlem19  45940  stoweidlem20  45941  stoweidlem21  45942  stoweidlem22  45943  stoweidlem23  45944  stoweidlem32  45953  stoweidlem36  45957  stoweidlem40  45961  stoweidlem41  45962  stoweidlem47  45968  stirlinglem15  46009  sge0ss  46333  sge0xp  46350  omeiunlempt  46441  hoicvrrex  46477  ovnlecvr2  46531  smfdiv  46718  smfneg  46724  smflimmpt  46731  smfsupmpt  46736  smfinfmpt  46740  smflimsuplem4  46744  smflimsuplem5  46745  smflimsupmpt  46750  smfliminf  46752  smfliminfmpt  46753