Theorem coeq2i 5724

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

Syntax hints:   = wceq 1536   ∘ ccom 5552

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 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2792

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-clab 2799  df-cleq 2813  df-clel 2892  df-nfc 2962  df-in 3936  df-ss 3945  df-br 5060  df-opab 5122  df-co 5557

This theorem is referenced by:  coeq12i  5727  cocnvcnv2  6104  co01  6107  fcoi1  6545  dftpos2  7902  tposco  7916  canthp1  10069  cats1co  14213  isoval  17030  mvdco  18568  evlsval  20294  evl1fval1lem  20488  evl1var  20494  pf1ind  20513  imasdsf1olem  22978  hoico1  29531  hoid1i  29564  pjclem1  29970  pjclem3  29972  pjci  29975  cycpmconjv  30805  cycpmconjs  30819  dfpo2  33012  poimirlem9  34936  cdlemk45  38116  cononrel1  40028  trclubgNEW  40052  trclrelexplem  40130  relexpaddss  40137  cotrcltrcl  40144  cortrcltrcl  40159  corclrtrcl  40160  cotrclrcl  40161  cortrclrcl  40162  cotrclrtrcl  40163  cortrclrtrcl  40164  brco3f1o  40457  clsneibex  40526  neicvgbex  40536  subsaliuncl  42715  meadjiun  42822  fundcmpsurinjimaid  43645