Theorem coeq2i 5803

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

Syntax hints:   = wceq 1540   ∘ ccom 5623

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 3920  df-br 5093  df-opab 5155  df-co 5628

This theorem is referenced by:  coeq12i  5806  cocnvcnv2  6207  co01  6210  dfpo2  6244  fcoi1  6698  f1ofvswap  7243  dftpos2  8176  tposco  8190  cottrcl  9615  canthp1  10548  cats1co  14763  isoval  17672  mvdco  19324  evlsval  21991  evl1fval1lem  22215  evl1var  22221  pf1ind  22240  rhmply1vr1  22272  rhmply1vsca  22273  imasdsf1olem  24259  hoico1  31700  hoid1i  31733  pjclem1  32139  pjclem3  32141  pjci  32144  cycpmconjv  33084  cycpmconjs  33098  poimirlem9  37613  cdlemk45  40930  cononrel1  43571  trclubgNEW  43595  trclrelexplem  43688  relexpaddss  43695  cotrcltrcl  43702  cortrcltrcl  43717  corclrtrcl  43718  cotrclrcl  43719  cortrclrcl  43720  cotrclrtrcl  43721  cortrclrtrcl  43722  brco3f1o  44010  clsneibex  44079  neicvgbex  44089  subsaliuncl  46343  meadjiun  46451  fundcmpsurinjimaid  47399  dftpos5  48862  tposrescnv  48867