Theorem mpteq2da 5201

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

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-12 2216  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-nf 1817  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-opab 5172  df-mpt 5191

This theorem is used by:  offval2f  7735  prodeq1f  16107  prodeq2ii  16112  gsumsnfd  20198  gsummoncoe1  22659  cayleyhamilton1  23243  xkocnv  24166  utopsnneiplem  24599  itgeq1f  26125  fpwrelmap  33398  gsummpt2d  33686  suppgsumssiun  33709  elrgspnsubrunlem2  33885  elrspunidl  34062  fedgmullem2  34345  esumf1o  34765  esum2d  34808  itg2addnclem  38794  ftc1anclem5  38820  mzpsubmpt  43958  mzpexpmpt  43960  refsum2cnlem1  46270  mpteq2dfa  46494  fmuldfeqlem1  46809  limsupval3  46917  liminfval5  46990  liminfvalxrmpt  47011  liminfval4  47014  limsupval4  47019  liminfvaluz2  47020  limsupvaluz4  47025  cncfiooicclem1  47118  dvmptfprodlem  47169  stoweidlem2  47227  stoweidlem6  47231  stoweidlem8  47233  stoweidlem17  47242  stoweidlem19  47244  stoweidlem20  47245  stoweidlem21  47246  stoweidlem22  47247  stoweidlem23  47248  stoweidlem32  47257  stoweidlem36  47261  stoweidlem40  47265  stoweidlem41  47266  stoweidlem47  47272  stirlinglem15  47313  sge0ss  47637  sge0xp  47654  omeiunlempt  47745  hoicvrrex  47781  ovnlecvr2  47835  smfdiv  48022  smfneg  48028  smflimmpt  48035  smfsupmpt  48040  smfinfmpt  48044  smflimsuplem4  48048  smflimsuplem5  48049  smflimsupmpt  48054  smfliminf  48056  smfliminfmpt  48057