Theorem mpteq1i 5206

Description: An equality theorem for the maps-to notation. (Contributed by Glauco Siliprandi, 17-Aug-2020.) Remove all disjoint variable conditions. (Revised by SN, 11-Nov-2024.)

Hypothesis

Ref	Expression
mpteq1i.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
mpteq1i	⊢ (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶)

Proof of Theorem mpteq1i

Step	Hyp	Ref	Expression
1		mpteq1i.1	. . . 4 ⊢ 𝐴 = 𝐵
2	1	a1i 11	. . 3 ⊢ (⊤ → 𝐴 = 𝐵)
3		eqidd 2732	. . 3 ⊢ (⊤ → 𝐶 = 𝐶)
4	2, 3	mpteq12dv 5201	. 2 ⊢ (⊤ → (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶))
5	4	mptru 1548	1 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶)

Syntax hints:   = wceq 1541  ⊤wtru 1542   ↦ cmpt 5193

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-opab 5173  df-mpt 5194

This theorem is referenced by:  fmptap  7121  mpompt  7475  offres  7921  mpomptsx  8001  mpompts  8002  pwfseq  10609  wrd2f1tovbij  14861  pmtrprfval  19283  gsum2dlem2  19762  gsumcom2  19766  srgbinomlem4  19974  ply1coe  21704  m2detleiblem3  22015  m2detleiblem4  22016  pmatcollpw3fi1lem1  22172  restco  22552  limcdif  25277  dfarea  26347  nosupcbv  27087  noinfcbv  27102  istrkg2ld  27465  wlknwwlksnbij  28896  wwlksnextbij  28910  clwlknf1oclwwlkn  29091  dfhnorm2  30127  trlset  38697  limsupequzmptlem  44089  sge0iunmptlemfi  44774  sge0iunmpt  44779  hoidmvlelem3  44958  smfmulc1  45157  smflimsuplem2  45182