Theorem mpteq1 5175

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

Syntax hints:   → wi 4   = wceq 1541   ↦ cmpt 5167

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-opab 5149  df-mpt 5168

This theorem is referenced by:  mpteq1d  5176  tposf12  8176  oarec  8472  wunex2  10624  wuncval2  10633  vrmdfval  18759  pmtrfval  19357  sylow1  19510  sylow2b  19530  sylow3lem5  19538  sylow3  19540  gsumconst  19841  gsum2dlem2  19878  gsumfsum  21366  mvrfval  21913  mplcoe1  21967  mplcoe5  21970  evlsval  22016  coe1fzgsumd  22214  evls1fval  22229  evl1gsumd  22267  mavmul0  22462  madugsum  22553  cramer0  22600  cnmpt1t  23575  cnmpt2t  23583  fmval  23853  symgtgp  24016  prdstgpd  24035  indv  32825  gsumvsca1  33187  gsumvsca2  33188  qusima  33365  qusrn  33366  nsgmgc  33369  nsgqusf1olem2  33371  gsumesum  34064  esumlub  34065  esum2d  34098  sitg0  34351  matunitlindflem1  37656  matunitlindf  37658  sdclem2  37782  evl1gprodd  42150  idomnnzgmulnz  42166  deg1gprod  42173  fsovcnvlem  44046  ntrneibex  44106  stoweidlem9  46047  sge0sn  46417  sge0iunmptlemfi  46451  sge0isum  46465  ovn02  46606