Theorem mpteq2da 5197

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1563  Ⅎwnf 1806   ∈ wcel 2145   ↦ cmpt 5186

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-12 2215  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-nf 1807  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-opab 5168  df-mpt 5187

This theorem is referenced by:  offval2f  7679  prodeq1f  15950  prodeq2ii  15955  gsumsnfd  20012  gsummoncoe1  22429  cayleyhamilton1  23010  xkocnv  23932  utopsnneiplem  24365  itgeq1f  25891  fpwrelmap  32990  gsummpt2d  33282  suppgsumssiun  33305  elrgspnsubrunlem2  33481  elrspunidl  33652  fedgmullem2  33937  esumf1o  34357  esum2d  34400  itg2addnclem  38182  ftc1anclem5  38208  mzpsubmpt  43336  mzpexpmpt  43338  refsum2cnlem1  45615  mpteq2dfa  45840  fmuldfeqlem1  46156  limsupval3  46264  liminfval5  46337  liminfvalxrmpt  46358  liminfval4  46361  limsupval4  46366  liminfvaluz2  46367  limsupvaluz4  46372  cncfiooicclem1  46465  dvmptfprodlem  46516  stoweidlem2  46574  stoweidlem6  46578  stoweidlem8  46580  stoweidlem17  46589  stoweidlem19  46591  stoweidlem20  46592  stoweidlem21  46593  stoweidlem22  46594  stoweidlem23  46595  stoweidlem32  46604  stoweidlem36  46608  stoweidlem40  46612  stoweidlem41  46613  stoweidlem47  46619  stirlinglem15  46660  sge0ss  46984  sge0xp  47001  omeiunlempt  47092  hoicvrrex  47128  ovnlecvr2  47182  smfdiv  47369  smfneg  47375  smflimmpt  47382  smfsupmpt  47387  smfinfmpt  47391  smflimsuplem4  47395  smflimsuplem5  47396  smflimsupmpt  47401  smfliminf  47403  smfliminfmpt  47404