Theorem coeq2i 5769

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

Hypothesis

Ref	Expression
coeq1i.1	⊢ 𝐴 = 𝐵

Assertion

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

Proof of Theorem coeq2i

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

Syntax hints:   = wceq 1539   ∘ ccom 5593

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-in 3894  df-ss 3904  df-br 5075  df-opab 5137  df-co 5598

This theorem is referenced by:  coeq12i  5772  cocnvcnv2  6162  co01  6165  dfpo2  6199  fcoi1  6648  f1ofvswap  7178  dftpos2  8059  tposco  8073  cottrcl  9477  canthp1  10410  cats1co  14569  isoval  17477  mvdco  19053  evlsval  21296  evl1fval1lem  21496  evl1var  21502  pf1ind  21521  imasdsf1olem  23526  hoico1  30118  hoid1i  30151  pjclem1  30557  pjclem3  30559  pjci  30562  cycpmconjv  31409  cycpmconjs  31423  poimirlem9  35786  cdlemk45  38961  cononrel1  41202  trclubgNEW  41226  trclrelexplem  41319  relexpaddss  41326  cotrcltrcl  41333  cortrcltrcl  41348  corclrtrcl  41349  cotrclrcl  41350  cortrclrcl  41351  cotrclrtrcl  41352  cortrclrtrcl  41353  brco3f1o  41643  clsneibex  41712  neicvgbex  41722  subsaliuncl  43897  meadjiun  44004  fundcmpsurinjimaid  44863