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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1537  Ⅎwnf 1780   ∈ wcel 2106   ↦ cmpt 5231

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-12 2175  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-nf 1781  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-opab 5211  df-mpt 5232

This theorem is referenced by:  mpteq2dvaOLD  5249  offval2f  7712  prodeq1f  15939  prodeq2ii  15944  gsumsnfd  19984  gsummoncoe1  22328  cayleyhamilton1  22914  xkocnv  23838  utopsnneiplem  24272  itgeq1f  25821  fpwrelmap  32751  gsummpt2d  33035  elrspunidl  33436  fedgmullem2  33658  esumf1o  34031  esum2d  34074  itg2addnclem  37658  ftc1anclem5  37684  mzpsubmpt  42731  mzpexpmpt  42733  refsum2cnlem1  44975  mpteq2dfa  45213  fmuldfeqlem1  45538  limsupval3  45648  liminfval5  45721  liminfvalxrmpt  45742  liminfval4  45745  limsupval4  45750  liminfvaluz2  45751  limsupvaluz4  45756  cncfiooicclem1  45849  dvmptfprodlem  45900  stoweidlem2  45958  stoweidlem6  45962  stoweidlem8  45964  stoweidlem17  45973  stoweidlem19  45975  stoweidlem20  45976  stoweidlem21  45977  stoweidlem22  45978  stoweidlem23  45979  stoweidlem32  45988  stoweidlem36  45992  stoweidlem40  45996  stoweidlem41  45997  stoweidlem47  46003  stirlinglem15  46044  sge0ss  46368  sge0xp  46385  omeiunlempt  46476  hoicvrrex  46512  ovnlecvr2  46566  smfdiv  46753  smfneg  46759  smflimmpt  46766  smfsupmpt  46771  smfinfmpt  46775  smflimsuplem4  46779  smflimsuplem5  46780  smflimsupmpt  46785  smfliminf  46787  smfliminfmpt  46788