Theorem coeq2i 5874

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

Syntax hints:   = wceq 1537   ∘ ccom 5693

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ss 3980  df-br 5149  df-opab 5211  df-co 5698

This theorem is referenced by:  coeq12i  5877  cocnvcnv2  6280  co01  6283  dfpo2  6318  fcoi1  6783  f1ofvswap  7326  dftpos2  8267  tposco  8281  cottrcl  9757  canthp1  10692  cats1co  14892  isoval  17813  mvdco  19478  evlsval  22128  evl1fval1lem  22350  evl1var  22356  pf1ind  22375  rhmply1vr1  22407  rhmply1vsca  22408  imasdsf1olem  24399  hoico1  31785  hoid1i  31818  pjclem1  32224  pjclem3  32226  pjci  32229  cycpmconjv  33145  cycpmconjs  33159  poimirlem9  37616  cdlemk45  40930  cononrel1  43584  trclubgNEW  43608  trclrelexplem  43701  relexpaddss  43708  cotrcltrcl  43715  cortrcltrcl  43730  corclrtrcl  43731  cotrclrcl  43732  cortrclrcl  43733  cotrclrtrcl  43734  cortrclrtrcl  43735  brco3f1o  44023  clsneibex  44092  neicvgbex  44102  subsaliuncl  46314  meadjiun  46422  fundcmpsurinjimaid  47336