Theorem coeq2i 5390

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

Syntax hints:   = wceq 1596   ∘ ccom 5222

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-clab 2711  df-cleq 2717  df-clel 2720  df-nfc 2855  df-in 3687  df-ss 3694  df-br 4761  df-opab 4821  df-co 5227

This theorem is referenced by:  coeq12i  5393  cocnvcnv2  5760  co01  5763  fcoi1  6191  dftpos2  7489  tposco  7503  canthp1  9589  cats1co  13722  isoval  16547  mvdco  17986  evlsval  19642  evl1fval1lem  19817  evl1var  19823  pf1ind  19842  imasdsf1olem  22300  hoico1  28845  hoid1i  28878  pjclem1  29284  pjclem3  29286  pjci  29289  dfpo2  31873  poimirlem9  33650  cdlemk45  36654  cononrel1  38319  trclubgNEW  38344  trclrelexplem  38422  relexpaddss  38429  cotrcltrcl  38436  cortrcltrcl  38451  corclrtrcl  38452  cotrclrcl  38453  cortrclrcl  38454  cotrclrtrcl  38455  cortrclrtrcl  38456  brco3f1o  38750  clsneibex  38819  neicvgbex  38829  subsaliuncl  40996  meadjiun  41103