Theorem mpteq1 5175

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 2738	. 2 ⊢ (𝐴 = 𝐵 → 𝐶 = 𝐶)
3	1, 2	mpteq12dv 5173	1 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶))

Syntax hints:   → wi 4   = wceq 1542   ↦ 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-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-opab 5149  df-mpt 5168

This theorem is referenced by:  mpteq1d  5176  tposf12  8192  oarec  8488  wunex2  10650  wuncval2  10659  vrmdfval  18782  pmtrfval  19383  sylow1  19536  sylow2b  19556  sylow3lem5  19564  sylow3  19566  gsumconst  19867  gsum2dlem2  19904  gsumfsum  21391  mvrfval  21937  mplcoe1  21993  mplcoe5  21996  evlsval  22042  coe1fzgsumd  22247  evls1fval  22262  evl1gsumd  22300  mavmul0  22495  madugsum  22586  cramer0  22633  cnmpt1t  23608  cnmpt2t  23616  fmval  23886  symgtgp  24049  prdstgpd  24068  indv  32914  suppgsumssiun  33138  gsumvsca1  33292  gsumvsca2  33293  domnprodeq0  33342  qusima  33473  qusrn  33474  nsgmgc  33477  nsgqusf1olem2  33479  deg1prod  33648  psrgsum  33697  psrmonprod  33701  vieta  33729  gsumesum  34209  esumlub  34210  esum2d  34243  sitg0  34496  matunitlindflem1  37928  matunitlindf  37930  sdclem2  38054  evl1gprodd  42548  idomnnzgmulnz  42564  deg1gprod  42571  fsovcnvlem  44443  ntrneibex  44503  stoweidlem9  46441  sge0sn  46811  sge0iunmptlemfi  46845  sge0isum  46859  ovn02  47000