Theorem coeq2i 5617

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

Syntax hints:   = wceq 1522   ∘ ccom 5447

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-ext 2769

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-in 3866  df-ss 3874  df-br 4963  df-opab 5025  df-co 5452

This theorem is referenced by:  coeq12i  5620  cocnvcnv2  5986  co01  5989  fcoi1  6420  dftpos2  7760  tposco  7774  canthp1  9922  cats1co  14054  isoval  16864  mvdco  18304  evlsval  19986  evl1fval1lem  20175  evl1var  20181  pf1ind  20200  imasdsf1olem  22666  hoico1  29224  hoid1i  29257  pjclem1  29663  pjclem3  29665  pjci  29668  cycpmconjv  30421  cycpmconjs  30436  dfpo2  32599  poimirlem9  34432  cdlemk45  37614  cononrel1  39439  trclubgNEW  39463  trclrelexplem  39541  relexpaddss  39548  cotrcltrcl  39555  cortrcltrcl  39570  corclrtrcl  39571  cotrclrcl  39572  cortrclrcl  39573  cotrclrtrcl  39574  cortrclrtrcl  39575  brco3f1o  39868  clsneibex  39937  neicvgbex  39947  subsaliuncl  42183  meadjiun  42290