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

Syntax hints:   = wceq 1547  ⊤wtru 1548   ↦ cmpt 5160

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-opab 5142  df-mpt 5161

This theorem is referenced by:  fmptap  7121  mpompt  7477  offres  7932  mpomptsx  8013  mpompts  8014  pwfseq  10585  wrd2f1tovbij  14920  pmtrprfval  19460  gsum2dlem2  19944  gsumcom2  19948  srgbinomlem4  20208  ply1coe  22291  m2detleiblem3  22619  m2detleiblem4  22620  pmatcollpw3fi1lem1  22776  restco  23154  limcdif  25868  dfarea  26949  nosupcbv  27691  noinfcbv  27706  istrkg2ld  28553  wlknwwlksnbij  29981  wwlksnextbij  29995  clwlknf1oclwwlkn  30179  dfhnorm2  31218  partfun2  32775  ccatws1f1o  33037  gsumwrd2dccat  33166  vietalem  33770  algextdeglem4  33911  algextdeglem5  33912  dfadjliftmap2  38831  dfblockliftmap2  38835  trlset  40660  limsupequzmptlem  46178  sge0iunmptlemfi  46863  sge0iunmpt  46868  hoidmvlelem3  47047  smfmulc1  47246  smflimsuplem2  47271  tposrescnv  49376  swapf1f1o  49772  precofval3  49868