Theorem mpteq1i 5196

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

This proof depends on syntax axioms:   = wceq 1570  ⊤wtru 1571   ↦ cmpt 5186

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-opab 5168  df-mpt 5187

This theorem is used by:  fmptap  7173  mpompt  7532  offres  7993  mpomptsx  8073  mpompts  8074  pwfseq  10742  wrd2f1tovbij  15106  pmtrprfval  19694  gsum2dlem2  20178  gsumcom2  20182  srgbinomlem4  20448  ply1coe  22609  m2detleiblem3  22937  m2detleiblem4  22938  pmatcollpw3fi1lem1  23097  restco  23475  limcdif  26189  dfarea  27281  nosupcbv  28052  noinfcbv  28067  istrkg2ld  28915  wlknwwlksnbij  30470  wwlksnextbij  30484  clwlknf1oclwwlkn  30668  dfhnorm2  31717  partfun2  33263  ccatws1f1o  33507  gsumwrd2dccat  33632  vietalem  34204  algextdeglem4  34345  algextdeglem5  34346  dfadjliftmap2  39369  dfblockliftmap2  39373  trlset  41198  limsupequzmptlem  46707  sge0iunmptlemfi  47392  sge0iunmpt  47397  hoidmvlelem3  47576  smfmulc1  47775  smflimsuplem2  47800  tposrescnv  49956  swapf1f1o  50352  precofval3  50448  dvsec  50825  dvcsc  50826  dvcot  50827