Theorem coeq1i 5694

Description: Equality inference for composition of two classes. (Contributed by NM, 16-Nov-2000.)

Hypothesis

Ref	Expression
coeq1i.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
coeq1i	⊢ (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶)

Proof of Theorem coeq1i

Step	Hyp	Ref	Expression
1		coeq1i.1	. 2 ⊢ 𝐴 = 𝐵
2		coeq1 5692	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶))
3	1, 2	ax-mp 5	1 ⊢ (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶)

Syntax hints:   = wceq 1538   ∘ ccom 5523

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898  df-br 5031  df-opab 5093  df-co 5528

This theorem is referenced by:  coeq12i  5698  cocnvcnv1  6077  hashgval  13689  imasdsval2  16781  prds1  19360  pf1mpf  20976  upxp  22228  uptx  22230  hoico2  29540  hoid1ri  29573  nmopcoadj2i  29885  pjclem3  29980  cycpmconjslem1  30846  cycpmconjs  30848  cyc3conja  30849  erdsze2lem2  32564  pprodcnveq  33457  diblss  38466  cononrel2  40295  trclubgNEW  40318  cortrcltrcl  40441  corclrtrcl  40442  cortrclrcl  40444  cotrclrtrcl  40445  cortrclrtrcl  40446  neicvgbex  40815  neicvgnvo  40818  dvsinax  42555