Theorem mpteq2da 5171

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1547  Ⅎwnf 1790   ∈ wcel 2119   ↦ cmpt 5160

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-12 2189  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-nf 1791  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-opab 5142  df-mpt 5161

This theorem is referenced by:  offval2f  7642  prodeq1f  15869  prodeq2ii  15874  gsumsnfd  19924  gsummoncoe1  22301  cayleyhamilton1  22882  xkocnv  23804  utopsnneiplem  24237  itgeq1f  25763  fpwrelmap  32832  gsummpt2d  33137  suppgsumssiun  33160  elrgspnsubrunlem2  33336  elrspunidl  33518  fedgmullem2  33821  esumf1o  34241  esum2d  34284  itg2addnclem  38045  ftc1anclem5  38071  mzpsubmpt  43199  mzpexpmpt  43201  refsum2cnlem1  45492  mpteq2dfa  45718  fmuldfeqlem1  46034  limsupval3  46142  liminfval5  46215  liminfvalxrmpt  46236  liminfval4  46239  limsupval4  46244  liminfvaluz2  46245  limsupvaluz4  46250  cncfiooicclem1  46343  dvmptfprodlem  46394  stoweidlem2  46452  stoweidlem6  46456  stoweidlem8  46458  stoweidlem17  46467  stoweidlem19  46469  stoweidlem20  46470  stoweidlem21  46471  stoweidlem22  46472  stoweidlem23  46473  stoweidlem32  46482  stoweidlem36  46486  stoweidlem40  46490  stoweidlem41  46491  stoweidlem47  46497  stirlinglem15  46538  sge0ss  46862  sge0xp  46879  omeiunlempt  46970  hoicvrrex  47006  ovnlecvr2  47060  smfdiv  47247  smfneg  47253  smflimmpt  47260  smfsupmpt  47265  smfinfmpt  47269  smflimsuplem4  47273  smflimsuplem5  47274  smflimsupmpt  47279  smfliminf  47281  smfliminfmpt  47282