Theorem mpteq2da 5201

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

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

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 2147  ax-9 2155  ax-12 2215  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-opab 5172  df-mpt 5191

This theorem is used by:  offval2f  7697  prodeq1f  15999  prodeq2ii  16004  gsumsnfd  20084  gsummoncoe1  22539  cayleyhamilton1  23123  xkocnv  24046  utopsnneiplem  24479  itgeq1f  26005  fpwrelmap  33212  gsummpt2d  33497  suppgsumssiun  33520  elrgspnsubrunlem2  33696  elrspunidl  33864  fedgmullem2  34148  esumf1o  34568  esum2d  34611  itg2addnclem  38428  ftc1anclem5  38454  mzpsubmpt  43596  mzpexpmpt  43598  refsum2cnlem1  45879  mpteq2dfa  46104  fmuldfeqlem1  46420  limsupval3  46528  liminfval5  46601  liminfvalxrmpt  46622  liminfval4  46625  limsupval4  46630  liminfvaluz2  46631  limsupvaluz4  46636  cncfiooicclem1  46729  dvmptfprodlem  46780  stoweidlem2  46838  stoweidlem6  46842  stoweidlem8  46844  stoweidlem17  46853  stoweidlem19  46855  stoweidlem20  46856  stoweidlem21  46857  stoweidlem22  46858  stoweidlem23  46859  stoweidlem32  46868  stoweidlem36  46872  stoweidlem40  46876  stoweidlem41  46877  stoweidlem47  46883  stirlinglem15  46924  sge0ss  47248  sge0xp  47265  omeiunlempt  47356  hoicvrrex  47392  ovnlecvr2  47446  smfdiv  47633  smfneg  47639  smflimmpt  47646  smfsupmpt  47651  smfinfmpt  47655  smflimsuplem4  47659  smflimsuplem5  47660  smflimsupmpt  47665  smfliminf  47667  smfliminfmpt  47668