Theorem mpteq1 5191

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

Syntax hints:   → wi 4   = wceq 1540   ↦ cmpt 5183

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-opab 5165  df-mpt 5184

This theorem is referenced by:  mpteq1d  5192  tposf12  8207  oarec  8503  wunex2  10667  wuncval2  10676  vrmdfval  18759  pmtrfval  19356  sylow1  19509  sylow2b  19529  sylow3lem5  19537  sylow3  19539  gsumconst  19840  gsum2dlem2  19877  gsumfsum  21327  mvrfval  21866  mplcoe1  21920  mplcoe5  21923  evlsval  21969  coe1fzgsumd  22167  evls1fval  22182  evl1gsumd  22220  mavmul0  22415  madugsum  22506  cramer0  22553  cnmpt1t  23528  cnmpt2t  23536  fmval  23806  symgtgp  23969  prdstgpd  23988  indv  32748  gsumvsca1  33152  gsumvsca2  33153  qusima  33352  qusrn  33353  nsgmgc  33356  nsgqusf1olem2  33358  gsumesum  34022  esumlub  34023  esum2d  34056  sitg0  34310  matunitlindflem1  37583  matunitlindf  37585  sdclem2  37709  evl1gprodd  42078  idomnnzgmulnz  42094  deg1gprod  42101  fsovcnvlem  43975  ntrneibex  44035  stoweidlem9  45980  sge0sn  46350  sge0iunmptlemfi  46384  sge0isum  46398  ovn02  46539