Theorem coeq2i 5840

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

Syntax hints:   = wceq 1540   ∘ ccom 5658

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ss 3943  df-br 5120  df-opab 5182  df-co 5663

This theorem is referenced by:  coeq12i  5843  cocnvcnv2  6247  co01  6250  dfpo2  6285  fcoi1  6752  f1ofvswap  7299  dftpos2  8242  tposco  8256  cottrcl  9733  canthp1  10668  cats1co  14875  isoval  17778  mvdco  19426  evlsval  22044  evl1fval1lem  22268  evl1var  22274  pf1ind  22293  rhmply1vr1  22325  rhmply1vsca  22326  imasdsf1olem  24312  hoico1  31737  hoid1i  31770  pjclem1  32176  pjclem3  32178  pjci  32181  cycpmconjv  33153  cycpmconjs  33167  poimirlem9  37653  cdlemk45  40966  cononrel1  43618  trclubgNEW  43642  trclrelexplem  43735  relexpaddss  43742  cotrcltrcl  43749  cortrcltrcl  43764  corclrtrcl  43765  cotrclrcl  43766  cortrclrcl  43767  cotrclrtrcl  43768  cortrclrtrcl  43769  brco3f1o  44057  clsneibex  44126  neicvgbex  44136  subsaliuncl  46387  meadjiun  46495  fundcmpsurinjimaid  47425  dftpos5  48849  tposrescnv  48854