Theorem coeq2i 5839

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ss 3897  df-br 5103  df-opab 5167  df-co 5660

This theorem is used by:  coeq12i  5842  cocnvcnv2  6263  co01  6266  dfpo2  6302  sbcfung  6568  fcoi1  6761  f1ofvswap  7318  dftpos2  8268  tposco  8282  cottrcl  9727  canthp1  10746  cats1co  15015  isoval  17949  mvdco  19668  evlsval  22404  evl1fval1lem  22657  evl1var  22663  pf1ind  22682  rhmply1vr1  22711  rhmply1vsca  22712  imasdsf1olem  24701  hoico1  32367  hoid1i  32400  pjclem1  32806  pjclem3  32808  pjci  32811  cycpmconjv  33753  cycpmconjs  33767  poimirlem9  38684  cdlemk45  42141  cononrel1  44731  trclubgNEW  44755  trclrelexplem  44848  relexpaddss  44855  cotrcltrcl  44862  cortrcltrcl  44877  corclrtrcl  44878  cotrclrcl  44879  cortrclrcl  44880  cotrclrtrcl  44881  cortrclrtrcl  44882  brco3f1o  45170  clsneibex  45239  neicvgbex  45249  subsaliuncl  47504  meadjiun  47612  fundcmpsurinjimaid  48629  dftpos5  50123  tposrescnv  50128