Theorem mpteq1i 5189

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

Syntax hints:   = wceq 1541  ⊤wtru 1542   ↦ cmpt 5179

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-opab 5161  df-mpt 5180

This theorem is referenced by:  fmptap  7116  mpompt  7472  offres  7927  mpomptsx  8008  mpompts  8009  pwfseq  10575  wrd2f1tovbij  14883  pmtrprfval  19416  gsum2dlem2  19900  gsumcom2  19904  srgbinomlem4  20164  ply1coe  22242  m2detleiblem3  22573  m2detleiblem4  22574  pmatcollpw3fi1lem1  22730  restco  23108  limcdif  25833  dfarea  26926  nosupcbv  27670  noinfcbv  27685  istrkg2ld  28532  wlknwwlksnbij  29961  wwlksnextbij  29975  clwlknf1oclwwlkn  30159  dfhnorm2  31197  partfun2  32755  ccatws1f1o  33033  gsumwrd2dccat  33160  vietalem  33735  algextdeglem4  33877  algextdeglem5  33878  dfadjliftmap2  38632  dfblockliftmap2  38635  trlset  40421  limsupequzmptlem  45972  sge0iunmptlemfi  46657  sge0iunmpt  46662  hoidmvlelem3  46841  smfmulc1  47040  smflimsuplem2  47065  tposrescnv  49124  swapf1f1o  49520  precofval3  49616