Theorem mpteq1 5161

Description: An equality theorem for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.) (Proof shortened by SN, 11-Nov-2024.)

Assertion

Ref	Expression
mpteq1	⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶))

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Allowed substitution hint:   𝐶(𝑥)

Proof of Theorem mpteq1

Step	Hyp	Ref	Expression
1		id 22	. 2 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵)
2		eqidd 2740	. 2 ⊢ (𝐴 = 𝐵 → 𝐶 = 𝐶)
3	1, 2	mpteq12dv 5159	1 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶))

Syntax hints:   → wi 4   = wceq 1547   ↦ cmpt 5153

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-opab 5135  df-mpt 5154

This theorem is referenced by:  mpteq1d  5162  tposf12  8191  oarec  8487  wunex2  10652  wuncval2  10661  indv  12152  vrmdfval  18815  pmtrfval  19416  sylow1  19569  sylow2b  19589  sylow3lem5  19597  sylow3  19599  gsumconst  19900  gsum2dlem2  19937  gsumfsum  21409  mvrfval  21955  mplcoe1  22013  mplcoe5  22016  evlsval  22062  coe1fzgsumd  22290  evls1fval  22305  evl1gsumd  22343  mavmul0  22535  madugsum  22626  cramer0  22673  cnmpt1t  23648  cnmpt2t  23656  fmval  23926  symgtgp  24089  prdstgpd  24108  suppgsumssiun  33153  gsumvsca1  33307  gsumvsca2  33308  domnprodeq0  33357  qusima  33491  qusrn  33492  nsgmgc  33495  nsgqusf1olem2  33497  deg1prod  33666  psrgsum  33732  psrmonprod  33736  vieta  33764  gsumesum  34243  esumlub  34244  esum2d  34277  sitg0  34530  matunitlindflem1  37983  matunitlindf  37985  sdclem2  38109  evl1gprodd  42602  idomnnzgmulnz  42618  deg1gprod  42625  fsovcnvlem  44457  ntrneibex  44517  stoweidlem9  46452  sge0sn  46822  sge0iunmptlemfi  46856  sge0isum  46870  ovn02  47011