Theorem coeq2i 5849

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

Syntax hints:   = wceq 1567   ∘ ccom 5668

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ss 3930  df-br 5114  df-opab 5178  df-co 5673

This theorem is referenced by:  coeq12i  5852  cocnvcnv2  6263  co01  6266  dfpo2  6300  fcoi1  6755  f1ofvswap  7307  dftpos2  8241  tposco  8255  cottrcl  9690  canthp1  10641  cats1co  14895  isoval  17824  mvdco  19517  evlsval  22208  evl1fval1lem  22461  evl1var  22467  pf1ind  22486  rhmply1vr1  22515  rhmply1vsca  22516  imasdsf1olem  24501  hoico1  32051  hoid1i  32084  pjclem1  32490  pjclem3  32492  pjci  32495  cycpmconjv  33405  cycpmconjs  33419  poimirlem9  38205  cdlemk45  41648  cononrel1  44249  trclubgNEW  44273  trclrelexplem  44366  relexpaddss  44373  cotrcltrcl  44380  cortrcltrcl  44395  corclrtrcl  44396  cotrclrcl  44397  cortrclrcl  44398  cotrclrtrcl  44399  cortrclrtrcl  44400  brco3f1o  44688  clsneibex  44757  neicvgbex  44767  subsaliuncl  47001  meadjiun  47109  fundcmpsurinjimaid  48086  dftpos5  49574  tposrescnv  49579