Theorem mpteq2da 5245

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

Syntax hints:   → wi 4   ∧ wa 394   = wceq 1539  Ⅎwnf 1783   ∈ wcel 2104   ↦ cmpt 5230

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-12 2169  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-opab 5210  df-mpt 5231

This theorem is referenced by:  mpteq2dvaOLD  5248  offval2f  7687  prodeq1f  15856  prodeq2ii  15861  gsumsnfd  19860  gsummoncoe1  22048  cayleyhamilton1  22614  xkocnv  23538  utopsnneiplem  23972  fpwrelmap  32225  gsummpt2d  32471  elrspunidl  32820  fedgmullem2  33003  esumf1o  33346  esum2d  33389  itg2addnclem  36842  ftc1anclem5  36868  mzpsubmpt  41783  mzpexpmpt  41785  refsum2cnlem1  44023  mpteq2dfa  44270  fmuldfeqlem1  44596  limsupval3  44706  liminfval5  44779  liminfvalxrmpt  44800  liminfval4  44803  limsupval4  44808  liminfvaluz2  44809  limsupvaluz4  44814  cncfiooicclem1  44907  dvmptfprodlem  44958  stoweidlem2  45016  stoweidlem6  45020  stoweidlem8  45022  stoweidlem17  45031  stoweidlem19  45033  stoweidlem20  45034  stoweidlem21  45035  stoweidlem22  45036  stoweidlem23  45037  stoweidlem32  45046  stoweidlem36  45050  stoweidlem40  45054  stoweidlem41  45055  stoweidlem47  45061  stirlinglem15  45102  sge0ss  45426  sge0xp  45443  omeiunlempt  45534  hoicvrrex  45570  ovnlecvr2  45624  smfdiv  45811  smfneg  45817  smflimmpt  45824  smfsupmpt  45829  smfinfmpt  45833  smflimsuplem4  45837  smflimsuplem5  45838  smflimsupmpt  45843  smfliminf  45845  smfliminfmpt  45846