Theorem coeq2i 5885

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

Syntax hints:   = wceq 1537   ∘ ccom 5704

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ss 3993  df-br 5167  df-opab 5229  df-co 5709

This theorem is referenced by:  coeq12i  5888  cocnvcnv2  6289  co01  6292  dfpo2  6327  fcoi1  6795  f1ofvswap  7342  dftpos2  8284  tposco  8298  cottrcl  9788  canthp1  10723  cats1co  14905  isoval  17826  mvdco  19487  evlsval  22133  evl1fval1lem  22355  evl1var  22361  pf1ind  22380  rhmply1vr1  22412  rhmply1vsca  22413  imasdsf1olem  24404  hoico1  31788  hoid1i  31821  pjclem1  32227  pjclem3  32229  pjci  32232  cycpmconjv  33135  cycpmconjs  33149  poimirlem9  37589  cdlemk45  40904  cononrel1  43556  trclubgNEW  43580  trclrelexplem  43673  relexpaddss  43680  cotrcltrcl  43687  cortrcltrcl  43702  corclrtrcl  43703  cotrclrcl  43704  cortrclrcl  43705  cotrclrtrcl  43706  cortrclrtrcl  43707  brco3f1o  43995  clsneibex  44064  neicvgbex  44074  subsaliuncl  46279  meadjiun  46387  fundcmpsurinjimaid  47285