Theorem mpteq2da 5239

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1539  Ⅎwnf 1782   ∈ wcel 2107   ↦ cmpt 5224

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-12 2176  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-nf 1783  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-opab 5205  df-mpt 5225

This theorem is referenced by:  mpteq2dvaOLD  5242  offval2f  7713  prodeq1f  15943  prodeq2ii  15948  gsumsnfd  19970  gsummoncoe1  22313  cayleyhamilton1  22899  xkocnv  23823  utopsnneiplem  24257  itgeq1f  25807  fpwrelmap  32745  gsummpt2d  33053  elrgspnsubrunlem2  33253  elrspunidl  33457  fedgmullem2  33682  esumf1o  34052  esum2d  34095  itg2addnclem  37679  ftc1anclem5  37705  mzpsubmpt  42759  mzpexpmpt  42761  refsum2cnlem1  45047  mpteq2dfa  45279  fmuldfeqlem1  45602  limsupval3  45712  liminfval5  45785  liminfvalxrmpt  45806  liminfval4  45809  limsupval4  45814  liminfvaluz2  45815  limsupvaluz4  45820  cncfiooicclem1  45913  dvmptfprodlem  45964  stoweidlem2  46022  stoweidlem6  46026  stoweidlem8  46028  stoweidlem17  46037  stoweidlem19  46039  stoweidlem20  46040  stoweidlem21  46041  stoweidlem22  46042  stoweidlem23  46043  stoweidlem32  46052  stoweidlem36  46056  stoweidlem40  46060  stoweidlem41  46061  stoweidlem47  46067  stirlinglem15  46108  sge0ss  46432  sge0xp  46449  omeiunlempt  46540  hoicvrrex  46576  ovnlecvr2  46630  smfdiv  46817  smfneg  46823  smflimmpt  46830  smfsupmpt  46835  smfinfmpt  46839  smflimsuplem4  46843  smflimsuplem5  46844  smflimsupmpt  46849  smfliminf  46851  smfliminfmpt  46852