Theorem mpteq1i 5202

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

This proof depends on syntax axioms:   = wceq 1570  ⊤wtru 1571   ↦ cmpt 5192

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-opab 5174  df-mpt 5193

This theorem is used by:  fmptap  7206  mpompt  7565  offres  8029  mpomptsx  8110  mpompts  8111  pwfseq  10788  wrd2f1tovbij  15156  pmtrprfval  19752  gsum2dlem2  20236  gsumcom2  20240  srgbinomlem4  20506  ply1coe  22671  m2detleiblem3  22999  m2detleiblem4  23000  pmatcollpw3fi1lem1  23159  restco  23537  limcdif  26251  dfarea  27345  nosupcbv  28116  noinfcbv  28131  istrkg2ld  28979  wlknwwlksnbij  30534  wwlksnextbij  30548  clwlknf1oclwwlkn  30732  dfhnorm2  31781  partfun2  33367  ccatws1f1o  33610  gsumwrd2dccat  33738  vietalem  34322  algextdeglem4  34463  algextdeglem5  34464  dfadjliftmap2  39655  dfblockliftmap2  39659  trlset  41484  limsupequzmptlem  47011  sge0iunmptlemfi  47696  sge0iunmpt  47701  hoidmvlelem3  47880  smfmulc1  48079  smflimsuplem2  48104  tposrescnv  50323  swapf1f1o  50728  precofval3  50837  dvsec  51284  dvcsc  51285  dvcot  51286