Theorem mpteq2da 5245

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1541  Ⅎwnf 1785   ∈ wcel 2106   ↦ cmpt 5230

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-12 2171  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-nf 1786  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-opab 5210  df-mpt 5231

This theorem is referenced by:  mpteq2dvaOLD  5248  offval2f  7681  prodeq1f  15848  prodeq2ii  15853  gsumsnfd  19813  gsummoncoe1  21819  cayleyhamilton1  22385  xkocnv  23309  utopsnneiplem  23743  fpwrelmap  31945  gsummpt2d  32188  elrspunidl  32534  fedgmullem2  32703  esumf1o  33036  esum2d  33079  itg2addnclem  36527  ftc1anclem5  36553  mzpsubmpt  41466  mzpexpmpt  41468  refsum2cnlem1  43706  mpteq2dfa  43958  fmuldfeqlem1  44284  limsupval3  44394  liminfval5  44467  liminfvalxrmpt  44488  liminfval4  44491  limsupval4  44496  liminfvaluz2  44497  limsupvaluz4  44502  cncfiooicclem1  44595  dvmptfprodlem  44646  stoweidlem2  44704  stoweidlem6  44708  stoweidlem8  44710  stoweidlem17  44719  stoweidlem19  44721  stoweidlem20  44722  stoweidlem21  44723  stoweidlem22  44724  stoweidlem23  44725  stoweidlem32  44734  stoweidlem36  44738  stoweidlem40  44742  stoweidlem41  44743  stoweidlem47  44749  stirlinglem15  44790  sge0ss  45114  sge0xp  45131  omeiunlempt  45222  hoicvrrex  45258  ovnlecvr2  45312  smfdiv  45499  smfneg  45505  smflimmpt  45512  smfsupmpt  45517  smfinfmpt  45521  smflimsuplem4  45525  smflimsuplem5  45526  smflimsupmpt  45531  smfliminf  45533  smfliminfmpt  45534