Theorem coeq2i 5706

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

Syntax hints:   = wceq 1538   ∘ ccom 5532

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-v 3411  df-in 3867  df-ss 3877  df-br 5037  df-opab 5099  df-co 5537

This theorem is referenced by:  coeq12i  5709  cocnvcnv2  6093  co01  6096  fcoi1  6542  f1ofvswap  7060  dftpos2  7925  tposco  7939  canthp1  10127  cats1co  14278  isoval  17108  mvdco  18654  evlsval  20863  evl1fval1lem  21063  evl1var  21069  pf1ind  21088  imasdsf1olem  23089  hoico1  29652  hoid1i  29685  pjclem1  30091  pjclem3  30093  pjci  30096  cycpmconjv  30948  cycpmconjs  30962  dfpo2  33251  poimirlem9  35381  cdlemk45  38558  cononrel1  40712  trclubgNEW  40736  trclrelexplem  40830  relexpaddss  40837  cotrcltrcl  40844  cortrcltrcl  40859  corclrtrcl  40860  cotrclrcl  40861  cortrclrcl  40862  cotrclrtrcl  40863  cortrclrtrcl  40864  brco3f1o  41154  clsneibex  41223  neicvgbex  41233  subsaliuncl  43409  meadjiun  43516  fundcmpsurinjimaid  44355