Theorem coeq2i 5847

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

Syntax hints:   = wceq 1567   ∘ ccom 5666

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 5671

This theorem is referenced by:  coeq12i  5850  cocnvcnv2  6261  co01  6264  dfpo2  6298  fcoi1  6753  f1ofvswap  7305  dftpos2  8239  tposco  8253  cottrcl  9688  canthp1  10639  cats1co  14893  isoval  17822  mvdco  19515  evlsval  22206  evl1fval1lem  22459  evl1var  22465  pf1ind  22484  rhmply1vr1  22513  rhmply1vsca  22514  imasdsf1olem  24499  hoico1  32049  hoid1i  32082  pjclem1  32488  pjclem3  32490  pjci  32493  cycpmconjv  33403  cycpmconjs  33417  poimirlem9  38168  cdlemk45  41611  cononrel1  44212  trclubgNEW  44236  trclrelexplem  44329  relexpaddss  44336  cotrcltrcl  44343  cortrcltrcl  44358  corclrtrcl  44359  cotrclrcl  44360  cortrclrcl  44361  cotrclrtrcl  44362  cortrclrtrcl  44363  brco3f1o  44651  clsneibex  44720  neicvgbex  44730  subsaliuncl  46964  meadjiun  47072  fundcmpsurinjimaid  48049  dftpos5  49537  tposrescnv  49542