Theorem mpteq1i 5203

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

Syntax hints:   = wceq 1570  ⊤wtru 1571   ↦ cmpt 5193

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-opab 5175  df-mpt 5194

This theorem is referenced by:  fmptap  7170  mpompt  7526  offres  7981  mpomptsx  8062  mpompts  8063  pwfseq  10650  wrd2f1tovbij  14999  pmtrprfval  19558  gsum2dlem2  20042  gsumcom2  20046  srgbinomlem4  20312  ply1coe  22439  m2detleiblem3  22767  m2detleiblem4  22768  pmatcollpw3fi1lem1  22924  restco  23302  limcdif  26016  dfarea  27106  nosupcbv  27847  noinfcbv  27862  istrkg2ld  28710  wlknwwlksnbij  30218  wwlksnextbij  30232  clwlknf1oclwwlkn  30416  dfhnorm2  31455  partfun2  33002  ccatws1f1o  33252  gsumwrd2dccat  33379  vietalem  33950  algextdeglem4  34091  algextdeglem5  34092  dfadjliftmap2  39087  dfblockliftmap2  39091  trlset  40916  limsupequzmptlem  46425  sge0iunmptlemfi  47110  sge0iunmpt  47115  hoidmvlelem3  47294  smfmulc1  47493  smflimsuplem2  47518  tposrescnv  49640  swapf1f1o  50036  precofval3  50132