Theorem mpteq1i 5188

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

Syntax hints:   = wceq 1540  ⊤wtru 1541   ↦ cmpt 5175

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2714  df-cleq 2728  df-clel 2814  df-opab 5155  df-mpt 5176

This theorem is referenced by:  fmptap  7098  mpompt  7450  offres  7894  mpomptsx  7972  mpompts  7973  pwfseq  10521  wrd2f1tovbij  14774  pmtrprfval  19191  gsum2dlem2  19667  gsumcom2  19671  srgbinomlem4  19874  ply1coe  21573  m2detleiblem3  21884  m2detleiblem4  21885  pmatcollpw3fi1lem1  22041  restco  22421  limcdif  25146  dfarea  26216  nosupcbv  26956  noinfcbv  26971  istrkg2ld  27110  wlknwwlksnbij  28541  wwlksnextbij  28555  clwlknf1oclwwlkn  28736  dfhnorm2  29772  trlset  38437  limsupequzmptlem  43614  sge0iunmptlemfi  44297  sge0iunmpt  44302  hoidmvlelem3  44481  smfmulc1  44680  smflimsuplem2  44705