Theorem mpteq2da 5185

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541  Ⅎwnf 1784   ∈ wcel 2113   ↦ cmpt 5174

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-12 2182  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-nf 1785  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-opab 5156  df-mpt 5175

This theorem is referenced by:  offval2f  7631  prodeq1f  15815  prodeq2ii  15820  gsumsnfd  19865  gsummoncoe1  22224  cayleyhamilton1  22808  xkocnv  23730  utopsnneiplem  24163  itgeq1f  25700  fpwrelmap  32720  gsummpt2d  33036  elrgspnsubrunlem2  33222  elrspunidl  33400  fedgmullem2  33664  esumf1o  34084  esum2d  34127  itg2addnclem  37731  ftc1anclem5  37757  mzpsubmpt  42860  mzpexpmpt  42862  refsum2cnlem1  45158  mpteq2dfa  45388  fmuldfeqlem1  45706  limsupval3  45814  liminfval5  45887  liminfvalxrmpt  45908  liminfval4  45911  limsupval4  45916  liminfvaluz2  45917  limsupvaluz4  45922  cncfiooicclem1  46015  dvmptfprodlem  46066  stoweidlem2  46124  stoweidlem6  46128  stoweidlem8  46130  stoweidlem17  46139  stoweidlem19  46141  stoweidlem20  46142  stoweidlem21  46143  stoweidlem22  46144  stoweidlem23  46145  stoweidlem32  46154  stoweidlem36  46158  stoweidlem40  46162  stoweidlem41  46163  stoweidlem47  46169  stirlinglem15  46210  sge0ss  46534  sge0xp  46551  omeiunlempt  46642  hoicvrrex  46678  ovnlecvr2  46732  smfdiv  46919  smfneg  46925  smflimmpt  46932  smfsupmpt  46937  smfinfmpt  46941  smflimsuplem4  46945  smflimsuplem5  46946  smflimsupmpt  46951  smfliminf  46953  smfliminfmpt  46954