Theorem coeq2i 5733

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

Syntax hints:   = wceq 1537   ∘ ccom 5561

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-in 3945  df-ss 3954  df-br 5069  df-opab 5131  df-co 5566

This theorem is referenced by:  coeq12i  5736  cocnvcnv2  6113  co01  6116  fcoi1  6554  dftpos2  7911  tposco  7925  canthp1  10078  cats1co  14220  isoval  17037  mvdco  18575  evlsval  20301  evl1fval1lem  20495  evl1var  20501  pf1ind  20520  imasdsf1olem  22985  hoico1  29535  hoid1i  29568  pjclem1  29974  pjclem3  29976  pjci  29979  cycpmconjv  30786  cycpmconjs  30800  dfpo2  32993  poimirlem9  34903  cdlemk45  38085  cononrel1  39961  trclubgNEW  39985  trclrelexplem  40063  relexpaddss  40070  cotrcltrcl  40077  cortrcltrcl  40092  corclrtrcl  40093  cotrclrcl  40094  cortrclrcl  40095  cotrclrtrcl  40096  cortrclrtrcl  40097  brco3f1o  40390  clsneibex  40459  neicvgbex  40469  subsaliuncl  42648  meadjiun  42755  fundcmpsurinjimaid  43578