Theorem mpteq1i 5014

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 5012	. 2 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶))
3	1, 2	ax-mp 5	1 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶)

Syntax hints:   = wceq 1508   ↦ cmpt 5005

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-12 2107  ax-ext 2745

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-clab 2754  df-cleq 2766  df-clel 2841  df-ral 3088  df-opab 4989  df-mpt 5006

This theorem is referenced by:  fmptap  6754  mpompt  7081  offres  7495  mpomptsx  7569  mpompts  7570  pwfseq  9883  wrd2f1tovbij  14184  pmtrprfval  18389  gsum2dlem2  18857  gsumcom2  18861  srgbinomlem4  19029  ply1coe  20183  m2detleiblem3  20958  m2detleiblem4  20959  pmatcollpw3fi1lem1  21114  restco  21492  limcdif  24193  dfarea  25256  istrkg2ld  25964  wlknwwlksnbij  27391  wwlksnextbij  27414  wwlksnextbijOLD  27415  clwlknf1oclwwlkn  27625  clwlknf1oclwwlknOLD  27627  dfhnorm2  28694  trlset  36775  limsupequzmptlem  41470  sge0iunmptlemfi  42156  sge0iunmpt  42161  hoidmvlelem3  42340  smfmulc1  42532  smflimsuplem2  42556