Theorem mpteq1 5174

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

Syntax hints:   → wi 4   = wceq 1542   ↦ cmpt 5166

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-opab 5148  df-mpt 5167

This theorem is referenced by:  mpteq1d  5175  tposf12  8201  oarec  8497  wunex2  10661  wuncval2  10670  indv  12161  vrmdfval  18824  pmtrfval  19425  sylow1  19578  sylow2b  19598  sylow3lem5  19606  sylow3  19608  gsumconst  19909  gsum2dlem2  19946  gsumfsum  21414  mvrfval  21959  mplcoe1  22015  mplcoe5  22018  evlsval  22064  coe1fzgsumd  22269  evls1fval  22284  evl1gsumd  22322  mavmul0  22517  madugsum  22608  cramer0  22655  cnmpt1t  23630  cnmpt2t  23638  fmval  23908  symgtgp  24071  prdstgpd  24090  suppgsumssiun  33133  gsumvsca1  33287  gsumvsca2  33288  domnprodeq0  33337  qusima  33468  qusrn  33469  nsgmgc  33472  nsgqusf1olem2  33474  deg1prod  33643  psrgsum  33692  psrmonprod  33696  vieta  33724  gsumesum  34203  esumlub  34204  esum2d  34237  sitg0  34490  matunitlindflem1  37937  matunitlindf  37939  sdclem2  38063  evl1gprodd  42556  idomnnzgmulnz  42572  deg1gprod  42579  fsovcnvlem  44440  ntrneibex  44500  stoweidlem9  46437  sge0sn  46807  sge0iunmptlemfi  46841  sge0isum  46855  ovn02  46996