Theorem mpteq1 5235

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

Syntax hints:   → wi 4   = wceq 1534   ↦ cmpt 5225

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-opab 5205  df-mpt 5226

This theorem is referenced by:  mpteq1d  5237  mpteq1iOLD  5239  tposf12  8250  oarec  8576  wunex2  10755  wuncval2  10764  vrmdfval  18801  pmtrfval  19398  sylow1  19551  sylow2b  19571  sylow3lem5  19579  sylow3  19581  gsumconst  19882  gsum2dlem2  19919  gsumfsum  21360  mvrfval  21916  mplcoe1  21968  mplcoe5  21971  evlsval  22025  coe1fzgsumd  22216  evls1fval  22231  evl1gsumd  22269  mavmul0  22447  madugsum  22538  cramer0  22585  cnmpt1t  23562  cnmpt2t  23570  fmval  23840  symgtgp  24003  prdstgpd  24022  gsumvsca1  32927  gsumvsca2  32928  qusima  33112  qusrn  33113  nsgmgc  33116  nsgqusf1olem2  33118  indv  33625  gsumesum  33672  esumlub  33673  esum2d  33706  sitg0  33960  matunitlindflem1  37083  matunitlindf  37085  sdclem2  37209  evl1gprodd  41582  idomnnzgmulnz  41598  deg1gprod  41606  fsovcnvlem  43437  ntrneibex  43497  stoweidlem9  45391  sge0sn  45761  sge0iunmptlemfi  45795  sge0isum  45809  ovn02  45950