Theorem coeq2i 5832

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

Syntax hints:   = wceq 1560   ∘ ccom 5651

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-ss 3921  df-br 5101  df-opab 5163  df-co 5656

This theorem is referenced by:  coeq12i  5835  cocnvcnv2  6246  co01  6249  dfpo2  6283  fcoi1  6738  f1ofvswap  7290  dftpos2  8223  tposco  8237  cottrcl  9674  canthp1  10612  cats1co  14869  isoval  17798  mvdco  19485  evlsval  22139  evl1fval1lem  22393  evl1var  22399  pf1ind  22418  rhmply1vr1  22447  rhmply1vsca  22448  imasdsf1olem  24433  hoico1  31959  hoid1i  31992  pjclem1  32398  pjclem3  32400  pjci  32403  cycpmconjv  33322  cycpmconjs  33336  poimirlem9  38128  cdlemk45  41571  cononrel1  44170  trclubgNEW  44194  trclrelexplem  44287  relexpaddss  44294  cotrcltrcl  44301  cortrcltrcl  44316  corclrtrcl  44317  cotrclrcl  44318  cortrclrcl  44319  cotrclrtrcl  44320  cortrclrtrcl  44321  brco3f1o  44609  clsneibex  44678  neicvgbex  44688  subsaliuncl  46932  meadjiun  47040  fundcmpsurinjimaid  48017  dftpos5  49495  tposrescnv  49500