Theorem mpteq1i 5170

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

Syntax hints:   = wceq 1539  ⊤wtru 1540   ↦ cmpt 5157

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-opab 5137  df-mpt 5158

This theorem is referenced by:  fmptap  7042  mpompt  7388  offres  7826  mpomptsx  7904  mpompts  7905  pwfseq  10420  wrd2f1tovbij  14675  pmtrprfval  19095  gsum2dlem2  19572  gsumcom2  19576  srgbinomlem4  19779  ply1coe  21467  m2detleiblem3  21778  m2detleiblem4  21779  pmatcollpw3fi1lem1  21935  restco  22315  limcdif  25040  dfarea  26110  istrkg2ld  26821  wlknwwlksnbij  28253  wwlksnextbij  28267  clwlknf1oclwwlkn  28448  dfhnorm2  29484  nosupcbv  33905  noinfcbv  33920  trlset  38175  limsupequzmptlem  43269  sge0iunmptlemfi  43951  sge0iunmpt  43956  hoidmvlelem3  44135  smfmulc1  44330  smflimsuplem2  44354