Theorem coeq2i 5838

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

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

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 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ss 3916  df-br 5104  df-opab 5168  df-co 5660

This theorem is used by:  coeq12i  5841  cocnvcnv2  6260  co01  6263  dfpo2  6299  sbcfung  6563  fcoi1  6756  f1ofvswap  7314  dftpos2  8260  tposco  8274  cottrcl  9720  canthp1  10739  cats1co  15007  isoval  17940  mvdco  19659  evlsval  22395  evl1fval1lem  22648  evl1var  22654  pf1ind  22673  rhmply1vr1  22702  rhmply1vsca  22703  imasdsf1olem  24692  hoico1  32358  hoid1i  32391  pjclem1  32797  pjclem3  32799  pjci  32802  cycpmconjv  33703  cycpmconjs  33717  poimirlem9  38547  cdlemk45  42004  cononrel1  44593  trclubgNEW  44617  trclrelexplem  44710  relexpaddss  44717  cotrcltrcl  44724  cortrcltrcl  44739  corclrtrcl  44740  cotrclrcl  44741  cortrclrcl  44742  cotrclrtrcl  44743  cortrclrtrcl  44744  brco3f1o  45032  clsneibex  45101  neicvgbex  45111  subsaliuncl  47367  meadjiun  47475  fundcmpsurinjimaid  48492  dftpos5  49981  tposrescnv  49986