Theorem mpteq1i 5188

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

Syntax hints:   = wceq 1559  ⊤wtru 1560   ↦ cmpt 5178

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-opab 5160  df-mpt 5179

This theorem is referenced by:  fmptap  7148  mpompt  7504  offres  7958  mpomptsx  8039  mpompts  8040  pwfseq  10615  wrd2f1tovbij  14966  pmtrprfval  19517  gsum2dlem2  20001  gsumcom2  20005  srgbinomlem4  20265  ply1coe  22348  m2detleiblem3  22676  m2detleiblem4  22677  pmatcollpw3fi1lem1  22833  restco  23211  limcdif  25925  dfarea  27012  nosupcbv  27753  noinfcbv  27768  istrkg2ld  28616  wlknwwlksnbij  30044  wwlksnextbij  30058  clwlknf1oclwwlkn  30242  dfhnorm2  31281  partfun2  32838  ccatws1f1o  33089  gsumwrd2dccat  33218  vietalem  33836  algextdeglem4  33977  algextdeglem5  33978  dfadjliftmap2  38916  dfblockliftmap2  38920  trlset  40745  limsupequzmptlem  46262  sge0iunmptlemfi  46947  sge0iunmpt  46952  hoidmvlelem3  47131  smfmulc1  47330  smflimsuplem2  47355  tposrescnv  49460  swapf1f1o  49856  precofval3  49952