Theorem mpteq1i 5177

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

Syntax hints:   = wceq 1542  ⊤wtru 1543   ↦ cmpt 5167

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-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-opab 5149  df-mpt 5168

This theorem is referenced by:  fmptap  7118  mpompt  7474  offres  7929  mpomptsx  8010  mpompts  8011  pwfseq  10578  wrd2f1tovbij  14913  pmtrprfval  19453  gsum2dlem2  19937  gsumcom2  19941  srgbinomlem4  20201  ply1coe  22273  m2detleiblem3  22604  m2detleiblem4  22605  pmatcollpw3fi1lem1  22761  restco  23139  limcdif  25853  dfarea  26937  nosupcbv  27680  noinfcbv  27695  istrkg2ld  28542  wlknwwlksnbij  29971  wwlksnextbij  29985  clwlknf1oclwwlkn  30169  dfhnorm2  31208  partfun2  32764  ccatws1f1o  33026  gsumwrd2dccat  33154  vietalem  33738  algextdeglem4  33880  algextdeglem5  33881  dfadjliftmap2  38792  dfblockliftmap2  38796  trlset  40621  limsupequzmptlem  46174  sge0iunmptlemfi  46859  sge0iunmpt  46864  hoidmvlelem3  47043  smfmulc1  47242  smflimsuplem2  47267  tposrescnv  49366  swapf1f1o  49762  precofval3  49858