Theorem coeq2i 5810

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

Syntax hints:   = wceq 1542   ∘ ccom 5629

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ss 3907  df-br 5087  df-opab 5149  df-co 5634

This theorem is referenced by:  coeq12i  5813  cocnvcnv2  6218  co01  6221  dfpo2  6255  fcoi1  6709  f1ofvswap  7255  dftpos2  8187  tposco  8201  cottrcl  9634  canthp1  10571  cats1co  14812  isoval  17726  mvdco  19414  evlsval  22077  evl1fval1lem  22308  evl1var  22314  pf1ind  22333  rhmply1vr1  22365  rhmply1vsca  22366  imasdsf1olem  24351  hoico1  31845  hoid1i  31878  pjclem1  32284  pjclem3  32286  pjci  32289  cycpmconjv  33221  cycpmconjs  33235  poimirlem9  37967  cdlemk45  41410  cononrel1  44042  trclubgNEW  44066  trclrelexplem  44159  relexpaddss  44166  cotrcltrcl  44173  cortrcltrcl  44188  corclrtrcl  44189  cotrclrcl  44190  cortrclrcl  44191  cotrclrtrcl  44192  cortrclrtrcl  44193  brco3f1o  44481  clsneibex  44550  neicvgbex  44560  subsaliuncl  46807  meadjiun  46915  fundcmpsurinjimaid  47886  dftpos5  49364  tposrescnv  49369