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  8194  oarec  8490  wunex2  10652  wuncval2  10661  indv  12152  vrmdfval  18815  pmtrfval  19416  sylow1  19569  sylow2b  19589  sylow3lem5  19597  sylow3  19599  gsumconst  19900  gsum2dlem2  19937  gsumfsum  21424  mvrfval  21969  mplcoe1  22025  mplcoe5  22028  evlsval  22074  coe1fzgsumd  22279  evls1fval  22294  evl1gsumd  22332  mavmul0  22527  madugsum  22618  cramer0  22665  cnmpt1t  23640  cnmpt2t  23648  fmval  23918  symgtgp  24081  prdstgpd  24100  suppgsumssiun  33148  gsumvsca1  33302  gsumvsca2  33303  domnprodeq0  33352  qusima  33483  qusrn  33484  nsgmgc  33487  nsgqusf1olem2  33489  deg1prod  33658  psrgsum  33707  psrmonprod  33711  vieta  33739  gsumesum  34219  esumlub  34220  esum2d  34253  sitg0  34506  matunitlindflem1  37951  matunitlindf  37953  sdclem2  38077  evl1gprodd  42570  idomnnzgmulnz  42586  deg1gprod  42593  fsovcnvlem  44458  ntrneibex  44518  stoweidlem9  46455  sge0sn  46825  sge0iunmptlemfi  46859  sge0isum  46873  ovn02  47014