Theorem coeq2i 5858

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

Syntax hints:   = wceq 1541   ∘ ccom 5679

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-in 3954  df-ss 3964  df-br 5148  df-opab 5210  df-co 5684

This theorem is referenced by:  coeq12i  5861  cocnvcnv2  6254  co01  6257  dfpo2  6292  fcoi1  6762  f1ofvswap  7300  dftpos2  8224  tposco  8238  cottrcl  9710  canthp1  10645  cats1co  14803  isoval  17708  mvdco  19307  evlsval  21640  evl1fval1lem  21840  evl1var  21846  pf1ind  21865  imasdsf1olem  23870  hoico1  30996  hoid1i  31029  pjclem1  31435  pjclem3  31437  pjci  31440  cycpmconjv  32288  cycpmconjs  32302  poimirlem9  36485  cdlemk45  39806  cononrel1  42330  trclubgNEW  42354  trclrelexplem  42447  relexpaddss  42454  cotrcltrcl  42461  cortrcltrcl  42476  corclrtrcl  42477  cotrclrcl  42478  cortrclrcl  42479  cotrclrtrcl  42480  cortrclrtrcl  42481  brco3f1o  42769  clsneibex  42838  neicvgbex  42848  subsaliuncl  45060  meadjiun  45168  fundcmpsurinjimaid  46065