Theorem mpteq1 5202

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

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

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 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-opab 5176  df-mpt 5195

This theorem is used by:  mpteq1d  5203  tposf12  8249  oarec  8549  wunex2  10734  wuncval2  10743  indv  12231  vrmdfval  18939  pmtrfval  19544  sylow1  19697  sylow2b  19717  sylow3lem5  19725  sylow3  19727  gsumconst  20028  gsum2dlem2  20065  gsumfsum  21614  mvrfval  22160  mplcoe1  22218  mplcoe5  22221  evlsval  22267  coe1fzgsumd  22494  evls1fval  22509  evl1gsumd  22547  mavmul0  22739  madugsum  22830  cramer0  22877  cnmpt1t  23853  cnmpt2t  23861  fmval  24131  symgtgp  24294  prdstgpd  24313  suppgsumssiun  33432  gsumvsca1  33586  gsumvsca2  33587  domnprodeq0  33639  qusima  33757  qusrn  33758  nsgmgc  33761  nsgqusf1olem2  33763  deg1prod  33913  psrgsum  33978  psrmonprod  33982  vieta  34010  gsumesum  34489  esumlub  34490  esum2d  34523  sitg0  34777  matunitlindflem1  38300  matunitlindf  38302  sdclem2  38426  evl1gprodd  42917  idomnnzgmulnz  42933  deg1gprod  42940  fsovcnvlem  44772  ntrneibex  44832  stoweidlem9  46756  sge0sn  47126  sge0iunmptlemfi  47160  sge0isum  47174  ovn02  47315