Theorem coeq2i 5861

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

Syntax hints:   = wceq 1542   ∘ ccom 5681

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966  df-br 5150  df-opab 5212  df-co 5686

This theorem is referenced by:  coeq12i  5864  cocnvcnv2  6258  co01  6261  dfpo2  6296  fcoi1  6766  f1ofvswap  7304  dftpos2  8228  tposco  8242  cottrcl  9714  canthp1  10649  cats1co  14807  isoval  17712  mvdco  19313  evlsval  21649  evl1fval1lem  21849  evl1var  21855  pf1ind  21874  imasdsf1olem  23879  hoico1  31040  hoid1i  31073  pjclem1  31479  pjclem3  31481  pjci  31484  cycpmconjv  32332  cycpmconjs  32346  poimirlem9  36545  cdlemk45  39866  cononrel1  42393  trclubgNEW  42417  trclrelexplem  42510  relexpaddss  42517  cotrcltrcl  42524  cortrcltrcl  42539  corclrtrcl  42540  cotrclrcl  42541  cortrclrcl  42542  cotrclrtrcl  42543  cortrclrtrcl  42544  brco3f1o  42832  clsneibex  42901  neicvgbex  42911  subsaliuncl  45122  meadjiun  45230  fundcmpsurinjimaid  46127