Theorem mpteq1i 5176

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-opab 5148  df-mpt 5167

This theorem is referenced by:  fmptap  7125  mpompt  7481  offres  7936  mpomptsx  8017  mpompts  8018  pwfseq  10587  wrd2f1tovbij  14922  pmtrprfval  19462  gsum2dlem2  19946  gsumcom2  19950  srgbinomlem4  20210  ply1coe  22263  m2detleiblem3  22594  m2detleiblem4  22595  pmatcollpw3fi1lem1  22751  restco  23129  limcdif  25843  dfarea  26924  nosupcbv  27666  noinfcbv  27681  istrkg2ld  28528  wlknwwlksnbij  29956  wwlksnextbij  29970  clwlknf1oclwwlkn  30154  dfhnorm2  31193  partfun2  32749  ccatws1f1o  33011  gsumwrd2dccat  33139  vietalem  33723  algextdeglem4  33864  algextdeglem5  33865  dfadjliftmap2  38778  dfblockliftmap2  38782  trlset  40607  limsupequzmptlem  46156  sge0iunmptlemfi  46841  sge0iunmpt  46846  hoidmvlelem3  47025  smfmulc1  47224  smflimsuplem2  47249  tposrescnv  49354  swapf1f1o  49750  precofval3  49846