Theorem mpteq1 5201

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

Syntax hints:   → wi 4   = wceq 1567   ↦ cmpt 5193

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-opab 5175  df-mpt 5194

This theorem is referenced by:  mpteq1d  5202  tposf12  8243  oarec  8543  wunex2  10719  wuncval2  10728  indv  12216  vrmdfval  18911  pmtrfval  19516  sylow1  19669  sylow2b  19689  sylow3lem5  19697  sylow3  19699  gsumconst  20000  gsum2dlem2  20037  gsumfsum  21549  mvrfval  22095  mplcoe1  22153  mplcoe5  22156  evlsval  22202  coe1fzgsumd  22429  evls1fval  22444  evl1gsumd  22482  mavmul0  22674  madugsum  22765  cramer0  22812  cnmpt1t  23787  cnmpt2t  23795  fmval  24065  symgtgp  24228  prdstgpd  24247  suppgsumssiun  33329  gsumvsca1  33483  gsumvsca2  33484  domnprodeq0  33536  qusima  33657  qusrn  33658  nsgmgc  33661  nsgqusf1olem2  33663  deg1prod  33814  psrgsum  33879  psrmonprod  33883  vieta  33911  gsumesum  34390  esumlub  34391  esum2d  34424  sitg0  34677  matunitlindflem1  38150  matunitlindf  38152  sdclem2  38276  evl1gprodd  42769  idomnnzgmulnz  42785  deg1gprod  42792  fsovcnvlem  44626  ntrneibex  44686  stoweidlem9  46610  sge0sn  46980  sge0iunmptlemfi  47014  sge0isum  47028  ovn02  47169