Theorem coeq1i 5847

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

This proof depends on syntax axioms:   = wceq 1570   ∘ ccom 5667

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ss 3923  df-br 5112  df-opab 5176  df-co 5672

This theorem is used by:  coeq12i  5851  cocnvcnv1  6261  ttrclco  9694  hashgval  14387  imasdsval2  17592  prds1  20450  pf1mpf  22562  upxp  23831  uptx  23833  hoico2  32180  hoid1ri  32213  nmopcoadj2i  32525  pjclem3  32620  cycpmconjslem1  33538  cycpmconjs  33540  cyc3conja  33541  1arithidomlem2  33890  selvascl  33971  erdsze2lem2  35733  pprodcnveq  36410  diblss  42002  cononrel2  44379  trclubgNEW  44402  cortrcltrcl  44524  corclrtrcl  44525  cortrclrcl  44527  cotrclrtrcl  44528  cortrclrtrcl  44529  neicvgbex  44896  neicvgnvo  44899  dvsinax  46685