Theorem mpteq1i 5195

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 5191	. 2 ⊢ (⊤ → (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶))
5	4	mptru 1570	1 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶)

Syntax hints:   = wceq 1563  ⊤wtru 1564   ↦ cmpt 5185

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-opab 5167  df-mpt 5186

This theorem is referenced by:  fmptap  7158  mpompt  7514  offres  7968  mpomptsx  8049  mpompts  8050  pwfseq  10637  wrd2f1tovbij  14985  pmtrprfval  19545  gsum2dlem2  20029  gsumcom2  20033  srgbinomlem4  20299  ply1coe  22415  m2detleiblem3  22743  m2detleiblem4  22744  pmatcollpw3fi1lem1  22900  restco  23278  limcdif  25992  dfarea  27079  nosupcbv  27820  noinfcbv  27835  istrkg2ld  28683  wlknwwlksnbij  30142  wwlksnextbij  30156  clwlknf1oclwwlkn  30340  dfhnorm2  31379  partfun2  32929  ccatws1f1o  33179  gsumwrd2dccat  33306  vietalem  33881  algextdeglem4  34022  algextdeglem5  34023  dfadjliftmap2  38963  dfblockliftmap2  38967  trlset  40792  limsupequzmptlem  46301  sge0iunmptlemfi  46986  sge0iunmpt  46991  hoidmvlelem3  47170  smfmulc1  47369  smflimsuplem2  47394  tposrescnv  49509  swapf1f1o  49905  precofval3  50001