Theorem mpteq1 5242

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

Syntax hints:   → wi 4   = wceq 1542   ↦ cmpt 5232

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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-opab 5212  df-mpt 5233

This theorem is referenced by:  mpteq1d  5244  mpteq1iOLD  5246  tposf12  8236  oarec  8562  wunex2  10733  wuncval2  10742  vrmdfval  18737  pmtrfval  19318  sylow1  19471  sylow2b  19491  sylow3lem5  19499  sylow3  19501  gsumconst  19802  gsum2dlem2  19839  gsumfsum  21012  mvrfval  21540  mplcoe1  21592  mplcoe5  21595  evlsval  21649  coe1fzgsumd  21826  evls1fval  21838  evl1gsumd  21876  mavmul0  22054  madugsum  22145  cramer0  22192  cnmpt1t  23169  cnmpt2t  23177  fmval  23447  symgtgp  23610  prdstgpd  23629  gsumvsca1  32402  gsumvsca2  32403  qusima  32550  qusrn  32551  nsgmgc  32554  nsgqusf1olem2  32556  indv  33041  gsumesum  33088  esumlub  33089  esum2d  33122  sitg0  33376  matunitlindflem1  36532  matunitlindf  36534  sdclem2  36658  fsovcnvlem  42812  ntrneibex  42872  stoweidlem9  44773  sge0sn  45143  sge0iunmptlemfi  45177  sge0isum  45191  ovn02  45332