Theorem mpteq1i 5191

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

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

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-opab 5163  df-mpt 5182

This theorem is referenced by:  fmptap  7126  mpompt  7482  offres  7937  mpomptsx  8018  mpompts  8019  pwfseq  10587  wrd2f1tovbij  14895  pmtrprfval  19428  gsum2dlem2  19912  gsumcom2  19916  srgbinomlem4  20176  ply1coe  22254  m2detleiblem3  22585  m2detleiblem4  22586  pmatcollpw3fi1lem1  22742  restco  23120  limcdif  25845  dfarea  26938  nosupcbv  27682  noinfcbv  27697  istrkg2ld  28544  wlknwwlksnbij  29973  wwlksnextbij  29987  clwlknf1oclwwlkn  30171  dfhnorm2  31209  partfun2  32765  ccatws1f1o  33043  gsumwrd2dccat  33171  vietalem  33755  algextdeglem4  33897  algextdeglem5  33898  dfadjliftmap2  38705  dfblockliftmap2  38709  trlset  40534  limsupequzmptlem  46083  sge0iunmptlemfi  46768  sge0iunmpt  46773  hoidmvlelem3  46952  smfmulc1  47151  smflimsuplem2  47176  tposrescnv  49235  swapf1f1o  49631  precofval3  49727