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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-opab 5158  df-mpt 5177

This theorem is referenced by:  fmptap  7112  mpompt  7468  offres  7923  mpomptsx  8004  mpompts  8005  pwfseq  10564  wrd2f1tovbij  14871  pmtrprfval  19403  gsum2dlem2  19887  gsumcom2  19891  srgbinomlem4  20151  ply1coe  22216  m2detleiblem3  22547  m2detleiblem4  22548  pmatcollpw3fi1lem1  22704  restco  23082  limcdif  25807  dfarea  26900  nosupcbv  27644  noinfcbv  27659  istrkg2ld  28441  wlknwwlksnbij  29870  wwlksnextbij  29884  clwlknf1oclwwlkn  30068  dfhnorm2  31106  partfun2  32663  ccatws1f1o  32941  gsumwrd2dccat  33056  algextdeglem4  33756  algextdeglem5  33757  dfadjliftmap2  38494  dfblockliftmap2  38497  trlset  40283  limsupequzmptlem  45853  sge0iunmptlemfi  46538  sge0iunmpt  46543  hoidmvlelem3  46722  smfmulc1  46921  smflimsuplem2  46946  tposrescnv  49006  swapf1f1o  49403  precofval3  49499