Theorem coeq2i 5814

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

Syntax hints:   = wceq 1540   ∘ ccom 5635

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ss 3928  df-br 5103  df-opab 5165  df-co 5640

This theorem is referenced by:  coeq12i  5817  cocnvcnv2  6219  co01  6222  dfpo2  6257  fcoi1  6716  f1ofvswap  7263  dftpos2  8199  tposco  8213  cottrcl  9648  canthp1  10583  cats1co  14798  isoval  17707  mvdco  19359  evlsval  22026  evl1fval1lem  22250  evl1var  22256  pf1ind  22275  rhmply1vr1  22307  rhmply1vsca  22308  imasdsf1olem  24294  hoico1  31735  hoid1i  31768  pjclem1  32174  pjclem3  32176  pjci  32179  cycpmconjv  33114  cycpmconjs  33128  poimirlem9  37616  cdlemk45  40934  cononrel1  43576  trclubgNEW  43600  trclrelexplem  43693  relexpaddss  43700  cotrcltrcl  43707  cortrcltrcl  43722  corclrtrcl  43723  cotrclrcl  43724  cortrclrcl  43725  cotrclrtrcl  43726  cortrclrtrcl  43727  brco3f1o  44015  clsneibex  44084  neicvgbex  44094  subsaliuncl  46349  meadjiun  46457  fundcmpsurinjimaid  47405  dftpos5  48855  tposrescnv  48860