Theorem mpteq1i 5186

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

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

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-opab 5158  df-mpt 5177

This theorem is referenced by:  fmptap  7110  mpompt  7467  offres  7925  mpomptsx  8006  mpompts  8007  pwfseq  10577  wrd2f1tovbij  14885  pmtrprfval  19384  gsum2dlem2  19868  gsumcom2  19872  srgbinomlem4  20132  ply1coe  22201  m2detleiblem3  22532  m2detleiblem4  22533  pmatcollpw3fi1lem1  22689  restco  23067  limcdif  25793  dfarea  26886  nosupcbv  27630  noinfcbv  27645  istrkg2ld  28423  wlknwwlksnbij  29851  wwlksnextbij  29865  clwlknf1oclwwlkn  30046  dfhnorm2  31084  ccatws1f1o  32906  gsumwrd2dccat  33033  algextdeglem4  33689  algextdeglem5  33690  trlset  40143  limsupequzmptlem  45713  sge0iunmptlemfi  46398  sge0iunmpt  46403  hoidmvlelem3  46582  smfmulc1  46781  smflimsuplem2  46806  tposrescnv  48867  swapf1f1o  49264  precofval3  49360