Theorem mpteq2da 5213

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

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

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 2007  ax-8 2110  ax-9 2118  ax-12 2177  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-nf 1784  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-opab 5182  df-mpt 5202

This theorem is referenced by:  offval2f  7684  prodeq1f  15920  prodeq2ii  15925  gsumsnfd  19930  gsummoncoe1  22244  cayleyhamilton1  22828  xkocnv  23750  utopsnneiplem  24184  itgeq1f  25722  fpwrelmap  32656  gsummpt2d  32989  elrgspnsubrunlem2  33189  elrspunidl  33389  fedgmullem2  33616  esumf1o  34027  esum2d  34070  itg2addnclem  37641  ftc1anclem5  37667  mzpsubmpt  42713  mzpexpmpt  42715  refsum2cnlem1  45009  mpteq2dfa  45239  fmuldfeqlem1  45559  limsupval3  45669  liminfval5  45742  liminfvalxrmpt  45763  liminfval4  45766  limsupval4  45771  liminfvaluz2  45772  limsupvaluz4  45777  cncfiooicclem1  45870  dvmptfprodlem  45921  stoweidlem2  45979  stoweidlem6  45983  stoweidlem8  45985  stoweidlem17  45994  stoweidlem19  45996  stoweidlem20  45997  stoweidlem21  45998  stoweidlem22  45999  stoweidlem23  46000  stoweidlem32  46009  stoweidlem36  46013  stoweidlem40  46017  stoweidlem41  46018  stoweidlem47  46024  stirlinglem15  46065  sge0ss  46389  sge0xp  46406  omeiunlempt  46497  hoicvrrex  46533  ovnlecvr2  46587  smfdiv  46774  smfneg  46780  smflimmpt  46787  smfsupmpt  46792  smfinfmpt  46796  smflimsuplem4  46800  smflimsuplem5  46801  smflimsupmpt  46806  smfliminf  46808  smfliminfmpt  46809