Theorem mpteq2da 5196

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1569  Ⅎwnf 1815   ∈ wcel 2144   ↦ cmpt 5185

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-12 2212  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-nf 1816  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-opab 5167  df-mpt 5186

This theorem is used by:  offval2f  7708  prodeq1f  16080  prodeq2ii  16085  gsumsnfd  20170  gsummoncoe1  22631  cayleyhamilton1  23215  xkocnv  24138  utopsnneiplem  24571  itgeq1f  26097  fpwrelmap  33371  gsummpt2d  33656  suppgsumssiun  33679  elrgspnsubrunlem2  33855  elrspunidl  34024  fedgmullem2  34308  esumf1o  34728  esum2d  34771  itg2addnclem  38682  ftc1anclem5  38708  mzpsubmpt  43847  mzpexpmpt  43849  refsum2cnlem1  46147  mpteq2dfa  46372  fmuldfeqlem1  46687  limsupval3  46795  liminfval5  46868  liminfvalxrmpt  46889  liminfval4  46892  limsupval4  46897  liminfvaluz2  46898  limsupvaluz4  46903  cncfiooicclem1  46996  dvmptfprodlem  47047  stoweidlem2  47105  stoweidlem6  47109  stoweidlem8  47111  stoweidlem17  47120  stoweidlem19  47122  stoweidlem20  47123  stoweidlem21  47124  stoweidlem22  47125  stoweidlem23  47126  stoweidlem32  47135  stoweidlem36  47139  stoweidlem40  47143  stoweidlem41  47144  stoweidlem47  47150  stirlinglem15  47191  sge0ss  47515  sge0xp  47532  omeiunlempt  47623  hoicvrrex  47659  ovnlecvr2  47713  smfdiv  47900  smfneg  47906  smflimmpt  47913  smfsupmpt  47918  smfinfmpt  47922  smflimsuplem4  47926  smflimsuplem5  47927  smflimsupmpt  47932  smfliminf  47934  smfliminfmpt  47935