Theorem mpteq2da 5208

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570  Ⅎwnf 1816   ∈ wcel 2146   ↦ cmpt 5197

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-12 2216  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-opab 5179  df-mpt 5198

This theorem is used by:  offval2f  7702  prodeq1f  15986  prodeq2ii  15991  gsumsnfd  20052  gsummoncoe1  22505  cayleyhamilton1  23086  xkocnv  24008  utopsnneiplem  24441  itgeq1f  25967  fpwrelmap  33115  gsummpt2d  33400  suppgsumssiun  33423  elrgspnsubrunlem2  33599  elrspunidl  33767  fedgmullem2  34051  esumf1o  34471  esum2d  34514  itg2addnclem  38363  ftc1anclem5  38389  mzpsubmpt  43515  mzpexpmpt  43517  refsum2cnlem1  45798  mpteq2dfa  46023  fmuldfeqlem1  46339  limsupval3  46447  liminfval5  46520  liminfvalxrmpt  46541  liminfval4  46544  limsupval4  46549  liminfvaluz2  46550  limsupvaluz4  46555  cncfiooicclem1  46648  dvmptfprodlem  46699  stoweidlem2  46757  stoweidlem6  46761  stoweidlem8  46763  stoweidlem17  46772  stoweidlem19  46774  stoweidlem20  46775  stoweidlem21  46776  stoweidlem22  46777  stoweidlem23  46778  stoweidlem32  46787  stoweidlem36  46791  stoweidlem40  46795  stoweidlem41  46796  stoweidlem47  46802  stirlinglem15  46843  sge0ss  47167  sge0xp  47184  omeiunlempt  47275  hoicvrrex  47311  ovnlecvr2  47365  smfdiv  47552  smfneg  47558  smflimmpt  47565  smfsupmpt  47570  smfinfmpt  47574  smflimsuplem4  47578  smflimsuplem5  47579  smflimsupmpt  47584  smfliminf  47586  smfliminfmpt  47587