Theorem coeq2i 5849

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

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ss 3901  df-br 5109  df-opab 5174  df-co 5667

This theorem is used by:  coeq12i  5852  cocnvcnv2  6279  co01  6284  dfpo2  6325  sbcfung  6591  fcoi1  6786  f1ofvswap  7345  dftpos2  8298  tposco  8312  cottrcl  9757  canthp1  10778  cats1co  15049  isoval  17990  mvdco  19710  evlsval  22450  evl1fval1lem  22703  evl1var  22709  pf1ind  22728  rhmply1vr1  22757  rhmply1vsca  22758  imasdsf1olem  24747  hoico1  32415  hoid1i  32448  pjclem1  32854  pjclem3  32856  pjci  32859  cycpmconjv  33802  cycpmconjs  33816  coss2b  38218  poimirlem9  38815  cdlemk45  42270  cononrel1  44855  trclubgNEW  44879  trclrelexplem  44972  relexpaddss  44979  cotrcltrcl  44986  cortrcltrcl  45001  corclrtrcl  45002  cotrclrcl  45003  cortrclrcl  45004  cotrclrtrcl  45005  cortrclrtrcl  45006  brco3f1o  45294  clsneibex  45363  neicvgbex  45373  subsaliuncl  47641  meadjiun  47749  fundcmpsurinjimaid  48766  dftpos5  50318  tposrescnv  50323