Theorem mpteq1 5235

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

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

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-opab 5206  df-mpt 5226

This theorem is referenced by:  mpteq1d  5237  mpteq1iOLD  5239  tposf12  8276  oarec  8600  wunex2  10778  wuncval2  10787  vrmdfval  18869  pmtrfval  19468  sylow1  19621  sylow2b  19641  sylow3lem5  19649  sylow3  19651  gsumconst  19952  gsum2dlem2  19989  gsumfsum  21452  mvrfval  22001  mplcoe1  22055  mplcoe5  22058  evlsval  22110  coe1fzgsumd  22308  evls1fval  22323  evl1gsumd  22361  mavmul0  22558  madugsum  22649  cramer0  22696  cnmpt1t  23673  cnmpt2t  23681  fmval  23951  symgtgp  24114  prdstgpd  24133  indv  32837  gsumvsca1  33232  gsumvsca2  33233  qusima  33436  qusrn  33437  nsgmgc  33440  nsgqusf1olem2  33442  gsumesum  34060  esumlub  34061  esum2d  34094  sitg0  34348  matunitlindflem1  37623  matunitlindf  37625  sdclem2  37749  evl1gprodd  42118  idomnnzgmulnz  42134  deg1gprod  42141  fsovcnvlem  44026  ntrneibex  44086  stoweidlem9  46024  sge0sn  46394  sge0iunmptlemfi  46428  sge0isum  46442  ovn02  46583