Theorem mpteq1 5240

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

Syntax hints:   → wi 4   = wceq 1536   ↦ cmpt 5230

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-opab 5210  df-mpt 5231

This theorem is referenced by:  mpteq1d  5242  mpteq1iOLD  5244  tposf12  8274  oarec  8598  wunex2  10775  wuncval2  10784  vrmdfval  18881  pmtrfval  19482  sylow1  19635  sylow2b  19655  sylow3lem5  19663  sylow3  19665  gsumconst  19966  gsum2dlem2  20003  gsumfsum  21469  mvrfval  22018  mplcoe1  22072  mplcoe5  22075  evlsval  22127  coe1fzgsumd  22323  evls1fval  22338  evl1gsumd  22376  mavmul0  22573  madugsum  22664  cramer0  22711  cnmpt1t  23688  cnmpt2t  23696  fmval  23966  symgtgp  24129  prdstgpd  24148  gsumvsca1  33214  gsumvsca2  33215  qusima  33415  qusrn  33416  nsgmgc  33419  nsgqusf1olem2  33421  indv  33992  gsumesum  34039  esumlub  34040  esum2d  34073  sitg0  34327  matunitlindflem1  37602  matunitlindf  37604  sdclem2  37728  evl1gprodd  42098  idomnnzgmulnz  42114  deg1gprod  42121  fsovcnvlem  44002  ntrneibex  44062  stoweidlem9  45964  sge0sn  46334  sge0iunmptlemfi  46368  sge0isum  46382  ovn02  46523