Theorem mpteq1 5259

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

Syntax hints:   → wi 4   = wceq 1537   ↦ cmpt 5249

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-opab 5229  df-mpt 5250

This theorem is referenced by:  mpteq1d  5261  mpteq1iOLD  5263  tposf12  8292  oarec  8618  wunex2  10807  wuncval2  10816  vrmdfval  18891  pmtrfval  19492  sylow1  19645  sylow2b  19665  sylow3lem5  19673  sylow3  19675  gsumconst  19976  gsum2dlem2  20013  gsumfsum  21475  mvrfval  22024  mplcoe1  22078  mplcoe5  22081  evlsval  22133  coe1fzgsumd  22329  evls1fval  22344  evl1gsumd  22382  mavmul0  22579  madugsum  22670  cramer0  22717  cnmpt1t  23694  cnmpt2t  23702  fmval  23972  symgtgp  24135  prdstgpd  24154  gsumvsca1  33205  gsumvsca2  33206  qusima  33401  qusrn  33402  nsgmgc  33405  nsgqusf1olem2  33407  indv  33976  gsumesum  34023  esumlub  34024  esum2d  34057  sitg0  34311  matunitlindflem1  37576  matunitlindf  37578  sdclem2  37702  evl1gprodd  42074  idomnnzgmulnz  42090  deg1gprod  42097  fsovcnvlem  43975  ntrneibex  44035  stoweidlem9  45930  sge0sn  46300  sge0iunmptlemfi  46334  sge0isum  46348  ovn02  46489