Theorem mpteq1 5186

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

Syntax hints:   → wi 4   = wceq 1559   ↦ cmpt 5178

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-opab 5160  df-mpt 5179

This theorem is referenced by:  mpteq1d  5187  tposf12  8225  oarec  8525  wunex2  10690  wuncval2  10699  indv  12191  vrmdfval  18881  pmtrfval  19481  sylow1  19634  sylow2b  19654  sylow3lem5  19662  sylow3  19664  gsumconst  19965  gsum2dlem2  20002  gsumfsum  21474  mvrfval  22020  mplcoe1  22078  mplcoe5  22081  evlsval  22127  coe1fzgsumd  22355  evls1fval  22370  evl1gsumd  22408  mavmul0  22600  madugsum  22691  cramer0  22738  cnmpt1t  23713  cnmpt2t  23721  fmval  23991  symgtgp  24154  prdstgpd  24173  suppgsumssiun  33213  gsumvsca1  33367  gsumvsca2  33368  domnprodeq0  33421  qusima  33555  qusrn  33556  nsgmgc  33559  nsgqusf1olem2  33561  deg1prod  33740  psrgsum  33806  psrmonprod  33810  vieta  33838  gsumesum  34317  esumlub  34318  esum2d  34351  sitg0  34604  matunitlindflem1  38076  matunitlindf  38078  sdclem2  38202  evl1gprodd  42695  idomnnzgmulnz  42711  deg1gprod  42718  fsovcnvlem  44550  ntrneibex  44610  stoweidlem9  46544  sge0sn  46914  sge0iunmptlemfi  46948  sge0isum  46962  ovn02  47103