Theorem mpteq2da 5218

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-opab 5187  df-mpt 5207

This theorem is referenced by:  offval2f  7691  prodeq1f  15927  prodeq2ii  15932  gsumsnfd  19937  gsummoncoe1  22251  cayleyhamilton1  22835  xkocnv  23757  utopsnneiplem  24191  itgeq1f  25729  fpwrelmap  32715  gsummpt2d  33048  elrgspnsubrunlem2  33248  elrspunidl  33448  fedgmullem2  33675  esumf1o  34086  esum2d  34129  itg2addnclem  37700  ftc1anclem5  37726  mzpsubmpt  42733  mzpexpmpt  42735  refsum2cnlem1  45028  mpteq2dfa  45258  fmuldfeqlem1  45578  limsupval3  45688  liminfval5  45761  liminfvalxrmpt  45782  liminfval4  45785  limsupval4  45790  liminfvaluz2  45791  limsupvaluz4  45796  cncfiooicclem1  45889  dvmptfprodlem  45940  stoweidlem2  45998  stoweidlem6  46002  stoweidlem8  46004  stoweidlem17  46013  stoweidlem19  46015  stoweidlem20  46016  stoweidlem21  46017  stoweidlem22  46018  stoweidlem23  46019  stoweidlem32  46028  stoweidlem36  46032  stoweidlem40  46036  stoweidlem41  46037  stoweidlem47  46043  stirlinglem15  46084  sge0ss  46408  sge0xp  46425  omeiunlempt  46516  hoicvrrex  46552  ovnlecvr2  46606  smfdiv  46793  smfneg  46799  smflimmpt  46806  smfsupmpt  46811  smfinfmpt  46815  smflimsuplem4  46819  smflimsuplem5  46820  smflimsupmpt  46825  smfliminf  46827  smfliminfmpt  46828