Theorem mpteq1 5199

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

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

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-opab 5173  df-mpt 5192

This theorem is referenced by:  mpteq1d  5200  tposf12  8233  oarec  8529  wunex2  10698  wuncval2  10707  vrmdfval  18790  pmtrfval  19387  sylow1  19540  sylow2b  19560  sylow3lem5  19568  sylow3  19570  gsumconst  19871  gsum2dlem2  19908  gsumfsum  21358  mvrfval  21897  mplcoe1  21951  mplcoe5  21954  evlsval  22000  coe1fzgsumd  22198  evls1fval  22213  evl1gsumd  22251  mavmul0  22446  madugsum  22537  cramer0  22584  cnmpt1t  23559  cnmpt2t  23567  fmval  23837  symgtgp  24000  prdstgpd  24019  indv  32782  gsumvsca1  33186  gsumvsca2  33187  qusima  33386  qusrn  33387  nsgmgc  33390  nsgqusf1olem2  33392  gsumesum  34056  esumlub  34057  esum2d  34090  sitg0  34344  matunitlindflem1  37617  matunitlindf  37619  sdclem2  37743  evl1gprodd  42112  idomnnzgmulnz  42128  deg1gprod  42135  fsovcnvlem  44009  ntrneibex  44069  stoweidlem9  46014  sge0sn  46384  sge0iunmptlemfi  46418  sge0isum  46432  ovn02  46573