Theorem mpteq1i 5130

Description: An equality theorem for the maps-to notation. (Contributed by Glauco Siliprandi, 17-Aug-2020.)

Hypothesis

Ref	Expression
mpteq1i.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
mpteq1i	⊢ (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶)

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Allowed substitution hint:   𝐶(𝑥)

Proof of Theorem mpteq1i

Step	Hyp	Ref	Expression
1		mpteq1i.1	. 2 ⊢ 𝐴 = 𝐵
2		mpteq1 5128	. 2 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶))
3	1, 2	ax-mp 5	1 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶)

Syntax hints:   = wceq 1543   ↦ cmpt 5120

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-10 2143  ax-12 2177  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-tru 1546  df-ex 1788  df-nf 1792  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-ral 3056  df-opab 5102  df-mpt 5121

This theorem is referenced by:  fmptap  6963  mpompt  7302  offres  7734  mpomptsx  7812  mpompts  7813  pwfseq  10243  wrd2f1tovbij  14492  pmtrprfval  18833  gsum2dlem2  19310  gsumcom2  19314  srgbinomlem4  19512  ply1coe  21171  m2detleiblem3  21480  m2detleiblem4  21481  pmatcollpw3fi1lem1  21637  restco  22015  limcdif  24727  dfarea  25797  istrkg2ld  26505  wlknwwlksnbij  27926  wwlksnextbij  27940  clwlknf1oclwwlkn  28121  dfhnorm2  29157  nosupcbv  33591  noinfcbv  33606  trlset  37861  limsupequzmptlem  42887  sge0iunmptlemfi  43569  sge0iunmpt  43574  hoidmvlelem3  43753  smfmulc1  43945  smflimsuplem2  43969