Theorem coeq2i 5438

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

Syntax hints:   = wceq 1632   ∘ ccom 5270

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-in 3722  df-ss 3729  df-br 4805  df-opab 4865  df-co 5275

This theorem is referenced by:  coeq12i  5441  cocnvcnv2  5808  co01  5811  fcoi1  6239  dftpos2  7539  tposco  7553  canthp1  9688  cats1co  13821  isoval  16646  mvdco  18085  evlsval  19741  evl1fval1lem  19916  evl1var  19922  pf1ind  19941  imasdsf1olem  22399  hoico1  28945  hoid1i  28978  pjclem1  29384  pjclem3  29386  pjci  29389  dfpo2  31973  poimirlem9  33749  cdlemk45  36755  cononrel1  38420  trclubgNEW  38445  trclrelexplem  38523  relexpaddss  38530  cotrcltrcl  38537  cortrcltrcl  38552  corclrtrcl  38553  cotrclrcl  38554  cortrclrcl  38555  cotrclrtrcl  38556  cortrclrtrcl  38557  brco3f1o  38851  clsneibex  38920  neicvgbex  38930  subsaliuncl  41097  meadjiun  41204