Theorem mpteq1 5189

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-opab 5163  df-mpt 5182

This theorem is referenced by:  mpteq1d  5190  tposf12  8203  oarec  8499  wunex2  10661  wuncval2  10670  vrmdfval  18793  pmtrfval  19391  sylow1  19544  sylow2b  19564  sylow3lem5  19572  sylow3  19574  gsumconst  19875  gsum2dlem2  19912  gsumfsum  21401  mvrfval  21948  mplcoe1  22004  mplcoe5  22007  evlsval  22053  coe1fzgsumd  22260  evls1fval  22275  evl1gsumd  22313  mavmul0  22508  madugsum  22599  cramer0  22646  cnmpt1t  23621  cnmpt2t  23629  fmval  23899  symgtgp  24062  prdstgpd  24081  indv  32942  suppgsumssiun  33166  gsumvsca1  33320  gsumvsca2  33321  domnprodeq0  33370  qusima  33501  qusrn  33502  nsgmgc  33505  nsgqusf1olem2  33507  deg1prod  33676  psrgsum  33725  psrmonprod  33729  vieta  33757  gsumesum  34237  esumlub  34238  esum2d  34271  sitg0  34524  matunitlindflem1  37867  matunitlindf  37869  sdclem2  37993  evl1gprodd  42487  idomnnzgmulnz  42503  deg1gprod  42510  fsovcnvlem  44369  ntrneibex  44429  stoweidlem9  46367  sge0sn  46737  sge0iunmptlemfi  46771  sge0isum  46785  ovn02  46926