Theorem coeq2i 5848

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

This proof depends on syntax axioms:   = wceq 1570   ∘ ccom 5667

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ss 3923  df-br 5112  df-opab 5176  df-co 5672

This theorem is used by:  coeq12i  5851  cocnvcnv2  6262  co01  6265  dfpo2  6301  fcoi1  6756  f1ofvswap  7313  dftpos2  8245  tposco  8259  cottrcl  9695  canthp1  10656  cats1co  14919  isoval  17846  mvdco  19561  evlsval  22289  evl1fval1lem  22542  evl1var  22548  pf1ind  22567  rhmply1vr1  22596  rhmply1vsca  22597  imasdsf1olem  24583  hoico1  32181  hoid1i  32214  pjclem1  32620  pjclem3  32622  pjci  32625  cycpmconjv  33528  cycpmconjs  33542  poimirlem9  38339  cdlemk45  41781  cononrel1  44380  trclubgNEW  44404  trclrelexplem  44497  relexpaddss  44504  cotrcltrcl  44511  cortrcltrcl  44526  corclrtrcl  44527  cotrclrcl  44528  cortrclrcl  44529  cotrclrtrcl  44530  cortrclrtrcl  44531  brco3f1o  44819  clsneibex  44888  neicvgbex  44898  subsaliuncl  47132  meadjiun  47240  fundcmpsurinjimaid  48220  dftpos5  49711  tposrescnv  49716