Theorem mpteq1 5167

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

Syntax hints:   → wi 4   = wceq 1539   ↦ cmpt 5157

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-opab 5137  df-mpt 5158

This theorem is referenced by:  mpteq1d  5169  mpteq1iOLD  5171  tposf12  8067  oarec  8393  wunex2  10494  wuncval2  10503  vrmdfval  18495  pmtrfval  19058  sylow1  19208  sylow2b  19228  sylow3lem5  19236  sylow3  19238  gsumconst  19535  gsum2dlem2  19572  gsumfsum  20665  mvrfval  21189  mplcoe1  21238  mplcoe5  21241  evlsval  21296  coe1fzgsumd  21473  evls1fval  21485  evl1gsumd  21523  mavmul0  21701  madugsum  21792  cramer0  21839  cnmpt1t  22816  cnmpt2t  22824  fmval  23094  symgtgp  23257  prdstgpd  23276  gsumvsca1  31479  gsumvsca2  31480  qusima  31594  nsgmgc  31597  nsgqusf1olem2  31599  indv  31980  gsumesum  32027  esumlub  32028  esum2d  32061  sitg0  32313  matunitlindflem1  35773  matunitlindf  35775  sdclem2  35900  fsovcnvlem  41621  ntrneibex  41683  stoweidlem9  43550  sge0sn  43917  sge0iunmptlemfi  43951  sge0isum  43965  ovn02  44106