Theorem mpteq1i 5201

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-opab 5173  df-mpt 5192

This theorem is referenced by:  fmptap  7147  mpompt  7506  offres  7965  mpomptsx  8046  mpompts  8047  pwfseq  10624  wrd2f1tovbij  14933  pmtrprfval  19424  gsum2dlem2  19908  gsumcom2  19912  srgbinomlem4  20145  ply1coe  22192  m2detleiblem3  22523  m2detleiblem4  22524  pmatcollpw3fi1lem1  22680  restco  23058  limcdif  25784  dfarea  26877  nosupcbv  27621  noinfcbv  27636  istrkg2ld  28394  wlknwwlksnbij  29825  wwlksnextbij  29839  clwlknf1oclwwlkn  30020  dfhnorm2  31058  ccatws1f1o  32880  gsumwrd2dccat  33014  algextdeglem4  33717  algextdeglem5  33718  trlset  40162  limsupequzmptlem  45733  sge0iunmptlemfi  46418  sge0iunmpt  46423  hoidmvlelem3  46602  smfmulc1  46801  smflimsuplem2  46826  tposrescnv  48871  swapf1f1o  49268  precofval3  49364