Theorem coeq2i 5871

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

Syntax hints:   = wceq 1540   ∘ ccom 5689

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ss 3968  df-br 5144  df-opab 5206  df-co 5694

This theorem is referenced by:  coeq12i  5874  cocnvcnv2  6278  co01  6281  dfpo2  6316  fcoi1  6782  f1ofvswap  7326  dftpos2  8268  tposco  8282  cottrcl  9759  canthp1  10694  cats1co  14895  isoval  17809  mvdco  19463  evlsval  22110  evl1fval1lem  22334  evl1var  22340  pf1ind  22359  rhmply1vr1  22391  rhmply1vsca  22392  imasdsf1olem  24383  hoico1  31775  hoid1i  31808  pjclem1  32214  pjclem3  32216  pjci  32219  cycpmconjv  33162  cycpmconjs  33176  poimirlem9  37636  cdlemk45  40949  cononrel1  43607  trclubgNEW  43631  trclrelexplem  43724  relexpaddss  43731  cotrcltrcl  43738  cortrcltrcl  43753  corclrtrcl  43754  cotrclrcl  43755  cortrclrcl  43756  cotrclrtrcl  43757  cortrclrtrcl  43758  brco3f1o  44046  clsneibex  44115  neicvgbex  44125  subsaliuncl  46373  meadjiun  46481  fundcmpsurinjimaid  47398  dftpos5  48774  tposrescnv  48779