Theorem mpteq1i 5198

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

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

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 5170  df-mpt 5189

This theorem is referenced by:  fmptap  7144  mpompt  7503  offres  7962  mpomptsx  8043  mpompts  8044  pwfseq  10617  wrd2f1tovbij  14926  pmtrprfval  19417  gsum2dlem2  19901  gsumcom2  19905  srgbinomlem4  20138  ply1coe  22185  m2detleiblem3  22516  m2detleiblem4  22517  pmatcollpw3fi1lem1  22673  restco  23051  limcdif  25777  dfarea  26870  nosupcbv  27614  noinfcbv  27629  istrkg2ld  28387  wlknwwlksnbij  29818  wwlksnextbij  29832  clwlknf1oclwwlkn  30013  dfhnorm2  31051  ccatws1f1o  32873  gsumwrd2dccat  33007  algextdeglem4  33710  algextdeglem5  33711  trlset  40155  limsupequzmptlem  45726  sge0iunmptlemfi  46411  sge0iunmpt  46416  hoidmvlelem3  46595  smfmulc1  46794  smflimsuplem2  46819  tposrescnv  48867  swapf1f1o  49264  precofval3  49360