Theorem mpteq1i 5262

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

Syntax hints:   = wceq 1537  ⊤wtru 1538   ↦ cmpt 5249

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-opab 5229  df-mpt 5250

This theorem is referenced by:  fmptap  7204  mpompt  7564  offres  8024  mpomptsx  8105  mpompts  8106  pwfseq  10733  wrd2f1tovbij  15009  pmtrprfval  19529  gsum2dlem2  20013  gsumcom2  20017  srgbinomlem4  20256  ply1coe  22323  m2detleiblem3  22656  m2detleiblem4  22657  pmatcollpw3fi1lem1  22813  restco  23193  limcdif  25931  dfarea  27021  nosupcbv  27765  noinfcbv  27780  istrkg2ld  28486  wlknwwlksnbij  29921  wwlksnextbij  29935  clwlknf1oclwwlkn  30116  dfhnorm2  31154  ccatws1f1o  32918  algextdeglem4  33711  algextdeglem5  33712  trlset  40118  limsupequzmptlem  45649  sge0iunmptlemfi  46334  sge0iunmpt  46339  hoidmvlelem3  46518  smfmulc1  46717  smflimsuplem2  46742