Theorem mpteq2da 5178

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 5169	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶))

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

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 5149  df-mpt 5168

This theorem is referenced by:  offval2f  7639  prodeq1f  15862  prodeq2ii  15867  gsumsnfd  19917  gsummoncoe1  22283  cayleyhamilton1  22867  xkocnv  23789  utopsnneiplem  24222  itgeq1f  25748  fpwrelmap  32821  gsummpt2d  33125  suppgsumssiun  33148  elrgspnsubrunlem2  33324  elrspunidl  33503  fedgmullem2  33790  esumf1o  34210  esum2d  34253  itg2addnclem  38006  ftc1anclem5  38032  mzpsubmpt  43189  mzpexpmpt  43191  refsum2cnlem1  45486  mpteq2dfa  45714  fmuldfeqlem1  46030  limsupval3  46138  liminfval5  46211  liminfvalxrmpt  46232  liminfval4  46235  limsupval4  46240  liminfvaluz2  46241  limsupvaluz4  46246  cncfiooicclem1  46339  dvmptfprodlem  46390  stoweidlem2  46448  stoweidlem6  46452  stoweidlem8  46454  stoweidlem17  46463  stoweidlem19  46465  stoweidlem20  46466  stoweidlem21  46467  stoweidlem22  46468  stoweidlem23  46469  stoweidlem32  46478  stoweidlem36  46482  stoweidlem40  46486  stoweidlem41  46487  stoweidlem47  46493  stirlinglem15  46534  sge0ss  46858  sge0xp  46875  omeiunlempt  46966  hoicvrrex  47002  ovnlecvr2  47056  smfdiv  47243  smfneg  47249  smflimmpt  47256  smfsupmpt  47261  smfinfmpt  47265  smflimsuplem4  47269  smflimsuplem5  47270  smflimsupmpt  47275  smfliminf  47277  smfliminfmpt  47278