Theorem mpteq1 5184

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

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

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 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-opab 5158  df-mpt 5177

This theorem is referenced by:  mpteq1d  5185  tposf12  8190  oarec  8486  wunex2  10640  wuncval2  10649  vrmdfval  18772  pmtrfval  19370  sylow1  19523  sylow2b  19543  sylow3lem5  19551  sylow3  19553  gsumconst  19854  gsum2dlem2  19891  gsumfsum  21380  mvrfval  21927  mplcoe1  21983  mplcoe5  21986  evlsval  22032  coe1fzgsumd  22239  evls1fval  22254  evl1gsumd  22292  mavmul0  22487  madugsum  22578  cramer0  22625  cnmpt1t  23600  cnmpt2t  23608  fmval  23878  symgtgp  24041  prdstgpd  24060  indv  32859  gsumvsca1  33236  gsumvsca2  33237  domnprodeq0  33286  qusima  33417  qusrn  33418  nsgmgc  33421  nsgqusf1olem2  33423  deg1prod  33592  vieta  33664  gsumesum  34144  esumlub  34145  esum2d  34178  sitg0  34431  matunitlindflem1  37729  matunitlindf  37731  sdclem2  37855  evl1gprodd  42283  idomnnzgmulnz  42299  deg1gprod  42306  fsovcnvlem  44170  ntrneibex  44230  stoweidlem9  46169  sge0sn  46539  sge0iunmptlemfi  46573  sge0isum  46587  ovn02  46728