Theorem coeq2i 5824

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

Syntax hints:   = wceq 1540   ∘ ccom 5642

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 3931  df-br 5108  df-opab 5170  df-co 5647

This theorem is referenced by:  coeq12i  5827  cocnvcnv2  6231  co01  6234  dfpo2  6269  fcoi1  6734  f1ofvswap  7281  dftpos2  8222  tposco  8236  cottrcl  9672  canthp1  10607  cats1co  14822  isoval  17727  mvdco  19375  evlsval  21993  evl1fval1lem  22217  evl1var  22223  pf1ind  22242  rhmply1vr1  22274  rhmply1vsca  22275  imasdsf1olem  24261  hoico1  31685  hoid1i  31718  pjclem1  32124  pjclem3  32126  pjci  32129  cycpmconjv  33099  cycpmconjs  33113  poimirlem9  37623  cdlemk45  40941  cononrel1  43583  trclubgNEW  43607  trclrelexplem  43700  relexpaddss  43707  cotrcltrcl  43714  cortrcltrcl  43729  corclrtrcl  43730  cotrclrcl  43731  cortrclrcl  43732  cotrclrtrcl  43733  cortrclrtrcl  43734  brco3f1o  44022  clsneibex  44091  neicvgbex  44101  subsaliuncl  46356  meadjiun  46464  fundcmpsurinjimaid  47412  dftpos5  48862  tposrescnv  48867