Theorem coeq2i 5814

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

Syntax hints:   = wceq 1540   ∘ ccom 5635

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ss 3928  df-br 5103  df-opab 5165  df-co 5640

This theorem is referenced by:  coeq12i  5817  cocnvcnv2  6219  co01  6222  dfpo2  6257  fcoi1  6716  f1ofvswap  7263  dftpos2  8199  tposco  8213  cottrcl  9648  canthp1  10583  cats1co  14798  isoval  17703  mvdco  19351  evlsval  21969  evl1fval1lem  22193  evl1var  22199  pf1ind  22218  rhmply1vr1  22250  rhmply1vsca  22251  imasdsf1olem  24237  hoico1  31658  hoid1i  31691  pjclem1  32097  pjclem3  32099  pjci  32102  cycpmconjv  33072  cycpmconjs  33086  poimirlem9  37596  cdlemk45  40914  cononrel1  43556  trclubgNEW  43580  trclrelexplem  43673  relexpaddss  43680  cotrcltrcl  43687  cortrcltrcl  43702  corclrtrcl  43703  cotrclrcl  43704  cortrclrcl  43705  cotrclrtrcl  43706  cortrclrtrcl  43707  brco3f1o  43995  clsneibex  44064  neicvgbex  44074  subsaliuncl  46329  meadjiun  46437  fundcmpsurinjimaid  47385  dftpos5  48835  tposrescnv  48840