Theorem coeq2i 5867

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

Syntax hints:   = wceq 1534   ∘ ccom 5686

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-ss 3964  df-br 5154  df-opab 5216  df-co 5691

This theorem is referenced by:  coeq12i  5870  cocnvcnv2  6269  co01  6272  dfpo2  6307  fcoi1  6776  f1ofvswap  7319  dftpos2  8258  tposco  8272  cottrcl  9762  canthp1  10697  cats1co  14865  isoval  17781  mvdco  19443  evlsval  22101  evl1fval1lem  22321  evl1var  22327  pf1ind  22346  rhmply1vr1  22378  rhmply1vsca  22379  imasdsf1olem  24370  hoico1  31689  hoid1i  31722  pjclem1  32128  pjclem3  32130  pjci  32133  cycpmconjv  33020  cycpmconjs  33034  poimirlem9  37330  cdlemk45  40646  cononrel1  43261  trclubgNEW  43285  trclrelexplem  43378  relexpaddss  43385  cotrcltrcl  43392  cortrcltrcl  43407  corclrtrcl  43408  cotrclrcl  43409  cortrclrcl  43410  cotrclrtrcl  43411  cortrclrtrcl  43412  brco3f1o  43700  clsneibex  43769  neicvgbex  43779  subsaliuncl  45979  meadjiun  46087  fundcmpsurinjimaid  46983