Theorem coeq2i 5817

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

Syntax hints:   = wceq 1542   ∘ ccom 5636

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ss 3920  df-br 5101  df-opab 5163  df-co 5641

This theorem is referenced by:  coeq12i  5820  cocnvcnv2  6225  co01  6228  dfpo2  6262  fcoi1  6716  f1ofvswap  7262  dftpos2  8195  tposco  8209  cottrcl  9640  canthp1  10577  cats1co  14791  isoval  17701  mvdco  19386  evlsval  22053  evl1fval1lem  22286  evl1var  22292  pf1ind  22311  rhmply1vr1  22343  rhmply1vsca  22344  imasdsf1olem  24329  hoico1  31844  hoid1i  31877  pjclem1  32283  pjclem3  32285  pjci  32288  cycpmconjv  33236  cycpmconjs  33250  poimirlem9  37880  cdlemk45  41323  cononrel1  43950  trclubgNEW  43974  trclrelexplem  44067  relexpaddss  44074  cotrcltrcl  44081  cortrcltrcl  44096  corclrtrcl  44097  cotrclrcl  44098  cortrclrcl  44099  cotrclrtrcl  44100  cortrclrtrcl  44101  brco3f1o  44389  clsneibex  44458  neicvgbex  44468  subsaliuncl  46716  meadjiun  46824  fundcmpsurinjimaid  47771  dftpos5  49233  tposrescnv  49238