Theorem coeq2i 5840

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

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

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 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ss 3916  df-br 5104  df-opab 5168  df-co 5664

This theorem is used by:  coeq12i  5843  cocnvcnv2  6255  co01  6258  dfpo2  6294  sbcfung  6557  fcoi1  6750  f1ofvswap  7308  dftpos2  8242  tposco  8256  cottrcl  9699  canthp1  10664  cats1co  14928  isoval  17855  mvdco  19573  evlsval  22303  evl1fval1lem  22556  evl1var  22562  pf1ind  22581  rhmply1vr1  22610  rhmply1vsca  22611  imasdsf1olem  24600  hoico1  32238  hoid1i  32271  pjclem1  32677  pjclem3  32679  pjci  32682  cycpmconjv  33583  cycpmconjs  33597  poimirlem9  38379  cdlemk45  41821  cononrel1  44435  trclubgNEW  44459  trclrelexplem  44552  relexpaddss  44559  cotrcltrcl  44566  cortrcltrcl  44581  corclrtrcl  44582  cotrclrcl  44583  cortrclrcl  44584  cotrclrtrcl  44585  cortrclrtrcl  44586  brco3f1o  44874  clsneibex  44943  neicvgbex  44953  subsaliuncl  47187  meadjiun  47295  fundcmpsurinjimaid  48312  dftpos5  49801  tposrescnv  49806