Theorem coeq2i 5204

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

Syntax hints:   = wceq 1475   ∘ ccom 5042

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-in 3547  df-ss 3554  df-br 4584  df-opab 4644  df-co 5047

This theorem is referenced by:  coeq12i  5207  cocnvcnv2  5564  co01  5567  fcoi1  5991  dftpos2  7256  tposco  7270  canthp1  9355  cats1co  13452  isoval  16248  mvdco  17688  evlsval  19340  evl1fval1lem  19515  evl1var  19521  pf1ind  19540  imasdsf1olem  21988  hoico1  27999  hoid1i  28032  pjclem1  28438  pjclem3  28440  pjci  28443  dfpo2  30898  poimirlem9  32588  cdlemk45  35253  cononrel1  36919  trclubgNEW  36944  trclrelexplem  37022  relexpaddss  37029  cotrcltrcl  37036  cortrcltrcl  37051  corclrtrcl  37052  cotrclrcl  37053  cortrclrcl  37054  cotrclrtrcl  37055  cortrclrtrcl  37056  brco3f1o  37351  clsneibex  37420  neicvgbex  37430  subsaliuncl  39252  meadjiun  39359