Theorem mpteq1i 5245

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

Syntax hints:   = wceq 1542  ⊤wtru 1543   ↦ cmpt 5232

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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-opab 5212  df-mpt 5233

This theorem is referenced by:  fmptap  7168  mpompt  7522  offres  7970  mpomptsx  8050  mpompts  8051  pwfseq  10659  wrd2f1tovbij  14911  pmtrprfval  19355  gsum2dlem2  19839  gsumcom2  19843  srgbinomlem4  20052  ply1coe  21820  m2detleiblem3  22131  m2detleiblem4  22132  pmatcollpw3fi1lem1  22288  restco  22668  limcdif  25393  dfarea  26465  nosupcbv  27205  noinfcbv  27220  istrkg2ld  27742  wlknwwlksnbij  29173  wwlksnextbij  29187  clwlknf1oclwwlkn  29368  dfhnorm2  30406  algextdeglem1  32803  trlset  39080  limsupequzmptlem  44492  sge0iunmptlemfi  45177  sge0iunmpt  45182  hoidmvlelem3  45361  smfmulc1  45560  smflimsuplem2  45585