Theorem coeq2i 5758

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

Syntax hints:   = wceq 1539   ∘ ccom 5584

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900  df-br 5071  df-opab 5133  df-co 5589

This theorem is referenced by:  coeq12i  5761  cocnvcnv2  6151  co01  6154  dfpo2  6188  fcoi1  6632  f1ofvswap  7158  dftpos2  8030  tposco  8044  canthp1  10341  cats1co  14497  isoval  17394  mvdco  18968  evlsval  21206  evl1fval1lem  21406  evl1var  21412  pf1ind  21431  imasdsf1olem  23434  hoico1  30019  hoid1i  30052  pjclem1  30458  pjclem3  30460  pjci  30463  cycpmconjv  31311  cycpmconjs  31325  cottrcl  33705  poimirlem9  35713  cdlemk45  38888  cononrel1  41091  trclubgNEW  41115  trclrelexplem  41208  relexpaddss  41215  cotrcltrcl  41222  cortrcltrcl  41237  corclrtrcl  41238  cotrclrcl  41239  cortrclrcl  41240  cotrclrtrcl  41241  cortrclrtrcl  41242  brco3f1o  41532  clsneibex  41601  neicvgbex  41611  subsaliuncl  43787  meadjiun  43894  fundcmpsurinjimaid  44751