Theorem coeq2i 5802

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

Syntax hints:   = wceq 1547   ∘ ccom 5622

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ss 3900  df-br 5073  df-opab 5135  df-co 5627

This theorem is referenced by:  coeq12i  5805  cocnvcnv2  6210  co01  6213  dfpo2  6247  fcoi1  6701  f1ofvswap  7250  dftpos2  8183  tposco  8197  cottrcl  9631  canthp1  10568  cats1co  14809  isoval  17723  mvdco  19411  evlsval  22062  evl1fval1lem  22316  evl1var  22322  pf1ind  22341  rhmply1vr1  22370  rhmply1vsca  22371  imasdsf1olem  24356  hoico1  31845  hoid1i  31878  pjclem1  32284  pjclem3  32286  pjci  32289  cycpmconjv  33223  cycpmconjs  33237  poimirlem9  37996  cdlemk45  41439  cononrel1  44038  trclubgNEW  44062  trclrelexplem  44155  relexpaddss  44162  cotrcltrcl  44169  cortrcltrcl  44184  corclrtrcl  44185  cotrclrcl  44186  cortrclrcl  44187  cotrclrtrcl  44188  cortrclrtrcl  44189  brco3f1o  44477  clsneibex  44546  neicvgbex  44556  subsaliuncl  46801  meadjiun  46909  fundcmpsurinjimaid  47886  dftpos5  49364  tposrescnv  49369