Theorem mpteq2da 5246

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540  Ⅎwnf 1784   ∈ wcel 2105   ↦ cmpt 5231

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-12 2170  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1781  df-nf 1785  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-opab 5211  df-mpt 5232

This theorem is referenced by:  mpteq2dvaOLD  5249  offval2f  7688  prodeq1f  15857  prodeq2ii  15862  gsumsnfd  19861  gsummoncoe1  22049  cayleyhamilton1  22615  xkocnv  23539  utopsnneiplem  23973  fpwrelmap  32226  gsummpt2d  32472  elrspunidl  32821  fedgmullem2  33004  esumf1o  33347  esum2d  33390  itg2addnclem  36843  ftc1anclem5  36869  mzpsubmpt  41784  mzpexpmpt  41786  refsum2cnlem1  44024  mpteq2dfa  44271  fmuldfeqlem1  44597  limsupval3  44707  liminfval5  44780  liminfvalxrmpt  44801  liminfval4  44804  limsupval4  44809  liminfvaluz2  44810  limsupvaluz4  44815  cncfiooicclem1  44908  dvmptfprodlem  44959  stoweidlem2  45017  stoweidlem6  45021  stoweidlem8  45023  stoweidlem17  45032  stoweidlem19  45034  stoweidlem20  45035  stoweidlem21  45036  stoweidlem22  45037  stoweidlem23  45038  stoweidlem32  45047  stoweidlem36  45051  stoweidlem40  45055  stoweidlem41  45056  stoweidlem47  45062  stirlinglem15  45103  sge0ss  45427  sge0xp  45444  omeiunlempt  45535  hoicvrrex  45571  ovnlecvr2  45625  smfdiv  45812  smfneg  45818  smflimmpt  45825  smfsupmpt  45830  smfinfmpt  45834  smflimsuplem4  45838  smflimsuplem5  45839  smflimsupmpt  45844  smfliminf  45846  smfliminfmpt  45847