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 2761	. . 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 2732

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

This theorem is used by:  fmptap  7168  mpompt  7527  offres  7980  mpomptsx  8061  mpompts  8062  pwfseq  10673  wrd2f1tovbij  15033  pmtrprfval  19614  gsum2dlem2  20098  gsumcom2  20102  srgbinomlem4  20368  ply1coe  22523  m2detleiblem3  22851  m2detleiblem4  22852  pmatcollpw3fi1lem1  23011  restco  23389  limcdif  26103  dfarea  27197  nosupcbv  27938  noinfcbv  27953  istrkg2ld  28801  wlknwwlksnbij  30356  wwlksnextbij  30370  clwlknf1oclwwlkn  30554  dfhnorm2  31603  partfun2  33149  ccatws1f1o  33393  gsumwrd2dccat  33518  vietalem  34089  algextdeglem4  34230  algextdeglem5  34231  dfadjliftmap2  39205  dfblockliftmap2  39209  trlset  41034  limsupequzmptlem  46556  sge0iunmptlemfi  47241  sge0iunmpt  47246  hoidmvlelem3  47425  smfmulc1  47624  smflimsuplem2  47649  tposrescnv  49805  swapf1f1o  50201  precofval3  50297  dvsec  50689  dvcsc  50690  dvcot  50691