Theorem mpteq1i 5211

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

Syntax hints:   = wceq 1540  ⊤wtru 1541   ↦ cmpt 5201

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-opab 5182  df-mpt 5202

This theorem is referenced by:  fmptap  7161  mpompt  7519  offres  7980  mpomptsx  8061  mpompts  8062  pwfseq  10676  wrd2f1tovbij  14977  pmtrprfval  19466  gsum2dlem2  19950  gsumcom2  19954  srgbinomlem4  20187  ply1coe  22234  m2detleiblem3  22565  m2detleiblem4  22566  pmatcollpw3fi1lem1  22722  restco  23100  limcdif  25827  dfarea  26920  nosupcbv  27664  noinfcbv  27679  istrkg2ld  28385  wlknwwlksnbij  29816  wwlksnextbij  29830  clwlknf1oclwwlkn  30011  dfhnorm2  31049  ccatws1f1o  32873  gsumwrd2dccat  33007  algextdeglem4  33700  algextdeglem5  33701  trlset  40126  limsupequzmptlem  45705  sge0iunmptlemfi  46390  sge0iunmpt  46395  hoidmvlelem3  46574  smfmulc1  46773  smflimsuplem2  46798  tposrescnv  48802  swapf1f1o  49140  precofval3  49230