Theorem coeq2i 5815

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

Syntax hints:   = wceq 1542   ∘ ccom 5635

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ss 3906  df-br 5086  df-opab 5148  df-co 5640

This theorem is referenced by:  coeq12i  5818  cocnvcnv2  6223  co01  6226  dfpo2  6260  fcoi1  6714  f1ofvswap  7261  dftpos2  8193  tposco  8207  cottrcl  9640  canthp1  10577  cats1co  14818  isoval  17732  mvdco  19420  evlsval  22064  evl1fval1lem  22295  evl1var  22301  pf1ind  22320  rhmply1vr1  22352  rhmply1vsca  22353  imasdsf1olem  24338  hoico1  31827  hoid1i  31860  pjclem1  32266  pjclem3  32268  pjci  32271  cycpmconjv  33203  cycpmconjs  33217  poimirlem9  37950  cdlemk45  41393  cononrel1  44021  trclubgNEW  44045  trclrelexplem  44138  relexpaddss  44145  cotrcltrcl  44152  cortrcltrcl  44167  corclrtrcl  44168  cotrclrcl  44169  cortrclrcl  44170  cotrclrtrcl  44171  cortrclrtrcl  44172  brco3f1o  44460  clsneibex  44529  neicvgbex  44539  subsaliuncl  46786  meadjiun  46894  fundcmpsurinjimaid  47871  dftpos5  49349  tposrescnv  49354