Theorem mpteq1i 5196

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

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

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-opab 5168  df-mpt 5187

This theorem is used by:  fmptap  7175  mpompt  7534  offres  7995  mpomptsx  8075  mpompts  8076  pwfseq  10749  wrd2f1tovbij  15113  pmtrprfval  19701  gsum2dlem2  20185  gsumcom2  20189  srgbinomlem4  20455  ply1coe  22616  m2detleiblem3  22944  m2detleiblem4  22945  pmatcollpw3fi1lem1  23104  restco  23482  limcdif  26196  dfarea  27288  nosupcbv  28059  noinfcbv  28074  istrkg2ld  28922  wlknwwlksnbij  30477  wwlksnextbij  30491  clwlknf1oclwwlkn  30675  dfhnorm2  31724  partfun2  33270  ccatws1f1o  33514  gsumwrd2dccat  33639  vietalem  34211  algextdeglem4  34352  algextdeglem5  34353  dfadjliftmap2  39390  dfblockliftmap2  39394  trlset  41219  limsupequzmptlem  46738  sge0iunmptlemfi  47423  sge0iunmpt  47428  hoidmvlelem3  47607  smfmulc1  47806  smflimsuplem2  47831  tposrescnv  49987  swapf1f1o  50383  precofval3  50479  dvsec  50856  dvcsc  50857  dvcot  50858