Theorem mpteq1i 5182

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

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

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 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-opab 5154  df-mpt 5173

This theorem is referenced by:  fmptap  7104  mpompt  7460  offres  7915  mpomptsx  7996  mpompts  7997  pwfseq  10555  wrd2f1tovbij  14867  pmtrprfval  19400  gsum2dlem2  19884  gsumcom2  19888  srgbinomlem4  20148  ply1coe  22214  m2detleiblem3  22545  m2detleiblem4  22546  pmatcollpw3fi1lem1  22702  restco  23080  limcdif  25805  dfarea  26898  nosupcbv  27642  noinfcbv  27657  istrkg2ld  28439  wlknwwlksnbij  29867  wwlksnextbij  29881  clwlknf1oclwwlkn  30062  dfhnorm2  31100  ccatws1f1o  32930  gsumwrd2dccat  33045  algextdeglem4  33731  algextdeglem5  33732  trlset  40206  limsupequzmptlem  45772  sge0iunmptlemfi  46457  sge0iunmpt  46462  hoidmvlelem3  46641  smfmulc1  46840  smflimsuplem2  46865  tposrescnv  48916  swapf1f1o  49313  precofval3  49409