Theorem mpteq1i 5204

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 2766	. . 3 ⊢ (⊤ → 𝐶 = 𝐶)
4	2, 3	mpteq12dv 5200	. 2 ⊢ (⊤ → (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶))
5	4	mptru 1577	1 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶)

This proof depends on syntax axioms:   = wceq 1570  ⊤wtru 1571   ↦ cmpt 5194

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-opab 5176  df-mpt 5195

This theorem is used by:  fmptap  7172  mpompt  7530  offres  7982  mpomptsx  8063  mpompts  8064  pwfseq  10660  wrd2f1tovbij  15016  pmtrprfval  19580  gsum2dlem2  20064  gsumcom2  20068  srgbinomlem4  20334  ply1coe  22487  m2detleiblem3  22815  m2detleiblem4  22816  pmatcollpw3fi1lem1  22972  restco  23350  limcdif  26064  dfarea  27154  nosupcbv  27895  noinfcbv  27910  istrkg2ld  28758  wlknwwlksnbij  30266  wwlksnextbij  30280  clwlknf1oclwwlkn  30464  dfhnorm2  31503  partfun2  33050  ccatws1f1o  33296  gsumwrd2dccat  33421  vietalem  33992  algextdeglem4  34133  algextdeglem5  34134  dfadjliftmap2  39139  dfblockliftmap2  39143  trlset  40968  limsupequzmptlem  46475  sge0iunmptlemfi  47160  sge0iunmpt  47165  hoidmvlelem3  47344  smfmulc1  47543  smflimsuplem2  47568  tposrescnv  49690  swapf1f1o  50086  precofval3  50182