Theorem mpteq2da 5199

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540  Ⅎwnf 1783   ∈ wcel 2109   ↦ cmpt 5188

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-12 2178  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-opab 5170  df-mpt 5189

This theorem is referenced by:  offval2f  7668  prodeq1f  15872  prodeq2ii  15877  gsumsnfd  19881  gsummoncoe1  22195  cayleyhamilton1  22779  xkocnv  23701  utopsnneiplem  24135  itgeq1f  25672  fpwrelmap  32656  gsummpt2d  32989  elrgspnsubrunlem2  33199  elrspunidl  33399  fedgmullem2  33626  esumf1o  34040  esum2d  34083  itg2addnclem  37665  ftc1anclem5  37691  mzpsubmpt  42731  mzpexpmpt  42733  refsum2cnlem1  45031  mpteq2dfa  45261  fmuldfeqlem1  45580  limsupval3  45690  liminfval5  45763  liminfvalxrmpt  45784  liminfval4  45787  limsupval4  45792  liminfvaluz2  45793  limsupvaluz4  45798  cncfiooicclem1  45891  dvmptfprodlem  45942  stoweidlem2  46000  stoweidlem6  46004  stoweidlem8  46006  stoweidlem17  46015  stoweidlem19  46017  stoweidlem20  46018  stoweidlem21  46019  stoweidlem22  46020  stoweidlem23  46021  stoweidlem32  46030  stoweidlem36  46034  stoweidlem40  46038  stoweidlem41  46039  stoweidlem47  46045  stirlinglem15  46086  sge0ss  46410  sge0xp  46427  omeiunlempt  46518  hoicvrrex  46554  ovnlecvr2  46608  smfdiv  46795  smfneg  46801  smflimmpt  46808  smfsupmpt  46813  smfinfmpt  46817  smflimsuplem4  46821  smflimsuplem5  46822  smflimsupmpt  46827  smfliminf  46829  smfliminfmpt  46830