Theorem mpteq1 5200

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

Syntax hints:   → wi 4   = wceq 1570   ↦ cmpt 5192

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-opab 5174  df-mpt 5193

This theorem is referenced by:  mpteq1d  5201  tposf12  8243  oarec  8543  wunex2  10718  wuncval2  10727  indv  12215  vrmdfval  18910  pmtrfval  19515  sylow1  19668  sylow2b  19688  sylow3lem5  19696  sylow3  19698  gsumconst  19999  gsum2dlem2  20036  gsumfsum  21584  mvrfval  22130  mplcoe1  22188  mplcoe5  22191  evlsval  22237  coe1fzgsumd  22464  evls1fval  22479  evl1gsumd  22517  mavmul0  22709  madugsum  22800  cramer0  22847  cnmpt1t  23822  cnmpt2t  23830  fmval  24100  symgtgp  24263  prdstgpd  24282  suppgsumssiun  33392  gsumvsca1  33546  gsumvsca2  33547  domnprodeq0  33599  qusima  33717  qusrn  33718  nsgmgc  33721  nsgqusf1olem2  33723  deg1prod  33873  psrgsum  33938  psrmonprod  33942  vieta  33970  gsumesum  34449  esumlub  34450  esum2d  34483  sitg0  34736  matunitlindflem1  38267  matunitlindf  38269  sdclem2  38393  evl1gprodd  42884  idomnnzgmulnz  42900  deg1gprod  42907  fsovcnvlem  44739  ntrneibex  44799  stoweidlem9  46723  sge0sn  47093  sge0iunmptlemfi  47127  sge0isum  47141  ovn02  47282