Theorem mpteq1i 5195

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

This proof depends on syntax axioms:   = wceq 1569  ⊤wtru 1570   ↦ cmpt 5185

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-opab 5167  df-mpt 5186

This theorem is used by:  fmptap  7176  mpompt  7535  offres  7996  mpomptsx  8076  mpompts  8077  pwfseq  10753  wrd2f1tovbij  15119  pmtrprfval  19707  gsum2dlem2  20191  gsumcom2  20195  srgbinomlem4  20461  ply1coe  22622  m2detleiblem3  22950  m2detleiblem4  22951  pmatcollpw3fi1lem1  23110  restco  23488  limcdif  26202  dfarea  27294  nosupcbv  28065  noinfcbv  28080  istrkg2ld  28928  wlknwwlksnbij  30483  wwlksnextbij  30497  clwlknf1oclwwlkn  30681  dfhnorm2  31730  partfun2  33318  ccatws1f1o  33561  gsumwrd2dccat  33686  vietalem  34258  algextdeglem4  34399  algextdeglem5  34400  dfadjliftmap2  39483  dfblockliftmap2  39487  trlset  41312  limsupequzmptlem  46832  sge0iunmptlemfi  47517  sge0iunmpt  47522  hoidmvlelem3  47701  smfmulc1  47900  smflimsuplem2  47925  tposrescnv  50086  swapf1f1o  50491  precofval3  50600  dvsec  51025  dvcsc  51026  dvcot  51027