Theorem mpteq1 5184

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

Syntax hints:   → wi 4   = wceq 1540   ↦ cmpt 5176

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-opab 5158  df-mpt 5177

This theorem is referenced by:  mpteq1d  5185  tposf12  8191  oarec  8487  wunex2  10651  wuncval2  10660  vrmdfval  18748  pmtrfval  19347  sylow1  19500  sylow2b  19520  sylow3lem5  19528  sylow3  19530  gsumconst  19831  gsum2dlem2  19868  gsumfsum  21359  mvrfval  21906  mplcoe1  21960  mplcoe5  21963  evlsval  22009  coe1fzgsumd  22207  evls1fval  22222  evl1gsumd  22260  mavmul0  22455  madugsum  22546  cramer0  22593  cnmpt1t  23568  cnmpt2t  23576  fmval  23846  symgtgp  24009  prdstgpd  24028  indv  32808  gsumvsca1  33181  gsumvsca2  33182  qusima  33358  qusrn  33359  nsgmgc  33362  nsgqusf1olem2  33364  gsumesum  34028  esumlub  34029  esum2d  34062  sitg0  34316  matunitlindflem1  37598  matunitlindf  37600  sdclem2  37724  evl1gprodd  42093  idomnnzgmulnz  42109  deg1gprod  42116  fsovcnvlem  43989  ntrneibex  44049  stoweidlem9  45994  sge0sn  46364  sge0iunmptlemfi  46398  sge0isum  46412  ovn02  46553