Theorem mpteq1 5163

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 5161	1 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶))

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-opab 5133  df-mpt 5154

This theorem is referenced by:  mpteq1d  5165  mpteq1iOLD  5167  tposf12  8038  oarec  8355  wunex2  10425  wuncval2  10434  vrmdfval  18410  pmtrfval  18973  sylow1  19123  sylow2b  19143  sylow3lem5  19151  sylow3  19153  gsumconst  19450  gsum2dlem2  19487  gsumfsum  20577  mvrfval  21099  mplcoe1  21148  mplcoe5  21151  evlsval  21206  coe1fzgsumd  21383  evls1fval  21395  evl1gsumd  21433  mavmul0  21609  madugsum  21700  cramer0  21747  cnmpt1t  22724  cnmpt2t  22732  fmval  23002  symgtgp  23165  prdstgpd  23184  gsumvsca1  31381  gsumvsca2  31382  qusima  31496  nsgmgc  31499  nsgqusf1olem2  31501  indv  31880  gsumesum  31927  esumlub  31928  esum2d  31961  sitg0  32213  matunitlindflem1  35700  matunitlindf  35702  sdclem2  35827  fsovcnvlem  41510  ntrneibex  41572  stoweidlem9  43440  sge0sn  43807  sge0iunmptlemfi  43841  sge0isum  43855  ovn02  43996