Theorem mpteq2da 5192

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542  Ⅎwnf 1785   ∈ wcel 2114   ↦ cmpt 5181

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-12 2185  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-nf 1786  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-opab 5163  df-mpt 5182

This theorem is referenced by:  offval2f  7647  prodeq1f  15841  prodeq2ii  15846  gsumsnfd  19892  gsummoncoe1  22264  cayleyhamilton1  22848  xkocnv  23770  utopsnneiplem  24203  itgeq1f  25740  fpwrelmap  32822  gsummpt2d  33142  suppgsumssiun  33165  elrgspnsubrunlem2  33341  elrspunidl  33520  fedgmullem2  33807  esumf1o  34227  esum2d  34270  itg2addnclem  37916  ftc1anclem5  37942  mzpsubmpt  43094  mzpexpmpt  43096  refsum2cnlem1  45391  mpteq2dfa  45619  fmuldfeqlem1  45936  limsupval3  46044  liminfval5  46117  liminfvalxrmpt  46138  liminfval4  46141  limsupval4  46146  liminfvaluz2  46147  limsupvaluz4  46152  cncfiooicclem1  46245  dvmptfprodlem  46296  stoweidlem2  46354  stoweidlem6  46358  stoweidlem8  46360  stoweidlem17  46369  stoweidlem19  46371  stoweidlem20  46372  stoweidlem21  46373  stoweidlem22  46374  stoweidlem23  46375  stoweidlem32  46384  stoweidlem36  46388  stoweidlem40  46392  stoweidlem41  46393  stoweidlem47  46399  stirlinglem15  46440  sge0ss  46764  sge0xp  46781  omeiunlempt  46872  hoicvrrex  46908  ovnlecvr2  46962  smfdiv  47149  smfneg  47155  smflimmpt  47162  smfsupmpt  47167  smfinfmpt  47171  smflimsuplem4  47175  smflimsuplem5  47176  smflimsupmpt  47181  smfliminf  47183  smfliminfmpt  47184