Theorem coeq2i 5827

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

Syntax hints:   = wceq 1540   ∘ ccom 5645

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ss 3934  df-br 5111  df-opab 5173  df-co 5650

This theorem is referenced by:  coeq12i  5830  cocnvcnv2  6234  co01  6237  dfpo2  6272  fcoi1  6737  f1ofvswap  7284  dftpos2  8225  tposco  8239  cottrcl  9679  canthp1  10614  cats1co  14829  isoval  17734  mvdco  19382  evlsval  22000  evl1fval1lem  22224  evl1var  22230  pf1ind  22249  rhmply1vr1  22281  rhmply1vsca  22282  imasdsf1olem  24268  hoico1  31692  hoid1i  31725  pjclem1  32131  pjclem3  32133  pjci  32136  cycpmconjv  33106  cycpmconjs  33120  poimirlem9  37630  cdlemk45  40948  cononrel1  43590  trclubgNEW  43614  trclrelexplem  43707  relexpaddss  43714  cotrcltrcl  43721  cortrcltrcl  43736  corclrtrcl  43737  cotrclrcl  43738  cortrclrcl  43739  cotrclrtrcl  43740  cortrclrtrcl  43741  brco3f1o  44029  clsneibex  44098  neicvgbex  44108  subsaliuncl  46363  meadjiun  46471  fundcmpsurinjimaid  47416  dftpos5  48866  tposrescnv  48871