Theorem mpteq1 5200

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ↦ cmpt 5192

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-opab 5174  df-mpt 5193

This theorem is used by:  mpteq1d  5201  tposf12  8306  oarec  8608  wunex2  10862  wuncval2  10871  indv  12362  vrmdfval  19102  pmtrfval  19715  sylow1  19868  sylow2b  19888  sylow3lem5  19896  sylow3  19898  gsumconst  20199  gsum2dlem2  20236  gsumfsum  21794  mvrfval  22343  mplcoe1  22401  mplcoe5  22404  evlsval  22450  coe1fzgsumd  22677  evls1fval  22692  evl1gsumd  22730  mavmul0  22922  madugsum  23013  matunitlindflem1  23049  matunitlindf  23051  cramer0  23063  cnmpt1t  24039  cnmpt2t  24047  fmval  24317  symgtgp  24480  prdstgpd  24499  suppgsumssiun  33732  gsumvsca1  33886  gsumvsca2  33887  domnprodeq0  33939  qusima  34063  qusrn  34064  nsgmgc  34067  nsgqusf1olem2  34069  deg1prod  34218  psrgsum  34291  psrmonprod  34295  vieta  34323  gsumesum  34802  esumlub  34803  esum2d  34836  sitg0  35089  sdclem2  38942  evl1gprodd  43433  idomnnzgmulnz  43449  deg1gprod  43456  fsovcnvlem  45274  ntrneibex  45334  stoweidlem9  47292  sge0sn  47662  sge0iunmptlemfi  47696  sge0isum  47710  ovn02  47851