Theorem mpteq1 5194

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ↦ cmpt 5186

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-opab 5168  df-mpt 5187

This theorem is used by:  mpteq1d  5195  tposf12  8261  oarec  8563  wunex2  10816  wuncval2  10825  indv  12315  vrmdfval  19045  pmtrfval  19657  sylow1  19810  sylow2b  19830  sylow3lem5  19838  sylow3  19840  gsumconst  20141  gsum2dlem2  20178  gsumfsum  21733  mvrfval  22281  mplcoe1  22339  mplcoe5  22342  evlsval  22388  coe1fzgsumd  22615  evls1fval  22630  evl1gsumd  22668  mavmul0  22860  madugsum  22951  matunitlindflem1  22987  matunitlindf  22989  cramer0  23001  cnmpt1t  23977  cnmpt2t  23985  fmval  24255  symgtgp  24418  prdstgpd  24437  suppgsumssiun  33626  gsumvsca1  33780  gsumvsca2  33781  domnprodeq0  33833  qusima  33952  qusrn  33953  nsgmgc  33956  nsgqusf1olem2  33958  deg1prod  34108  psrgsum  34173  psrmonprod  34177  vieta  34205  gsumesum  34684  esumlub  34685  esum2d  34718  sitg0  34971  sdclem2  38656  evl1gprodd  43147  idomnnzgmulnz  43163  deg1gprod  43170  fsovcnvlem  44998  ntrneibex  45058  stoweidlem9  46988  sge0sn  47358  sge0iunmptlemfi  47392  sge0isum  47406  ovn02  47547