Theorem coeq2i 5807

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

Syntax hints:   = wceq 1541   ∘ ccom 5626

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-ss 3916  df-br 5097  df-opab 5159  df-co 5631

This theorem is referenced by:  coeq12i  5810  cocnvcnv2  6215  co01  6218  dfpo2  6252  fcoi1  6706  f1ofvswap  7250  dftpos2  8183  tposco  8197  cottrcl  9626  canthp1  10563  cats1co  14777  isoval  17687  mvdco  19372  evlsval  22039  evl1fval1lem  22272  evl1var  22278  pf1ind  22297  rhmply1vr1  22329  rhmply1vsca  22330  imasdsf1olem  24315  hoico1  31780  hoid1i  31813  pjclem1  32219  pjclem3  32221  pjci  32224  cycpmconjv  33173  cycpmconjs  33187  poimirlem9  37769  cdlemk45  41146  cononrel1  43777  trclubgNEW  43801  trclrelexplem  43894  relexpaddss  43901  cotrcltrcl  43908  cortrcltrcl  43923  corclrtrcl  43924  cotrclrcl  43925  cortrclrcl  43926  cotrclrtrcl  43927  cortrclrtrcl  43928  brco3f1o  44216  clsneibex  44285  neicvgbex  44295  subsaliuncl  46544  meadjiun  46652  fundcmpsurinjimaid  47599  dftpos5  49061  tposrescnv  49066