Theorem mpteq1i 5238

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-opab 5206  df-mpt 5226

This theorem is referenced by:  fmptap  7190  mpompt  7547  offres  8008  mpomptsx  8089  mpompts  8090  pwfseq  10704  wrd2f1tovbij  14999  pmtrprfval  19505  gsum2dlem2  19989  gsumcom2  19993  srgbinomlem4  20226  ply1coe  22302  m2detleiblem3  22635  m2detleiblem4  22636  pmatcollpw3fi1lem1  22792  restco  23172  limcdif  25911  dfarea  27003  nosupcbv  27747  noinfcbv  27762  istrkg2ld  28468  wlknwwlksnbij  29908  wwlksnextbij  29922  clwlknf1oclwwlkn  30103  dfhnorm2  31141  ccatws1f1o  32936  gsumwrd2dccat  33070  algextdeglem4  33761  algextdeglem5  33762  trlset  40163  limsupequzmptlem  45743  sge0iunmptlemfi  46428  sge0iunmpt  46433  hoidmvlelem3  46612  smfmulc1  46811  smflimsuplem2  46836  tposrescnv  48779  swapf1f1o  48981  precoffunc  49066