Theorem coeq2i 5846

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

Syntax hints:   = wceq 1570   ∘ ccom 5665

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ss 3922  df-br 5110  df-opab 5174  df-co 5670

This theorem is referenced by:  coeq12i  5849  cocnvcnv2  6260  co01  6263  dfpo2  6297  fcoi1  6752  f1ofvswap  7304  dftpos2  8235  tposco  8249  cottrcl  9684  canthp1  10634  cats1co  14889  isoval  17817  mvdco  19510  evlsval  22237  evl1fval1lem  22490  evl1var  22496  pf1ind  22515  rhmply1vr1  22544  rhmply1vsca  22545  imasdsf1olem  24530  hoico1  32108  hoid1i  32141  pjclem1  32547  pjclem3  32549  pjci  32552  cycpmconjv  33462  cycpmconjs  33476  poimirlem9  38300  cdlemk45  41741  cononrel1  44340  trclubgNEW  44364  trclrelexplem  44457  relexpaddss  44464  cotrcltrcl  44471  cortrcltrcl  44486  corclrtrcl  44487  cotrclrcl  44488  cortrclrcl  44489  cotrclrtrcl  44490  cortrclrtrcl  44491  brco3f1o  44779  clsneibex  44848  neicvgbex  44858  subsaliuncl  47092  meadjiun  47200  fundcmpsurinjimaid  48180  dftpos5  49672  tposrescnv  49677