Theorem mpteq2da 5197

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570  Ⅎwnf 1816   ∈ wcel 2145   ↦ cmpt 5186

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-12 2213  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-opab 5168  df-mpt 5187

This theorem is used by:  offval2f  7697  prodeq1f  16055  prodeq2ii  16060  gsumsnfd  20145  gsummoncoe1  22606  cayleyhamilton1  23190  xkocnv  24113  utopsnneiplem  24546  itgeq1f  26072  fpwrelmap  33307  gsummpt2d  33592  suppgsumssiun  33615  elrgspnsubrunlem2  33791  elrspunidl  33960  fedgmullem2  34244  esumf1o  34664  esum2d  34707  itg2addnclem  38557  ftc1anclem5  38583  mzpsubmpt  43707  mzpexpmpt  43709  refsum2cnlem1  45997  mpteq2dfa  46222  fmuldfeqlem1  46538  limsupval3  46646  liminfval5  46719  liminfvalxrmpt  46740  liminfval4  46743  limsupval4  46748  liminfvaluz2  46749  limsupvaluz4  46754  cncfiooicclem1  46847  dvmptfprodlem  46898  stoweidlem2  46956  stoweidlem6  46960  stoweidlem8  46962  stoweidlem17  46971  stoweidlem19  46973  stoweidlem20  46974  stoweidlem21  46975  stoweidlem22  46976  stoweidlem23  46977  stoweidlem32  46986  stoweidlem36  46990  stoweidlem40  46994  stoweidlem41  46995  stoweidlem47  47001  stirlinglem15  47042  sge0ss  47366  sge0xp  47383  omeiunlempt  47474  hoicvrrex  47510  ovnlecvr2  47564  smfdiv  47751  smfneg  47757  smflimmpt  47764  smfsupmpt  47769  smfinfmpt  47773  smflimsuplem4  47777  smflimsuplem5  47778  smflimsupmpt  47783  smfliminf  47785  smfliminfmpt  47786