MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  coeq2i Unicode version

Theorem coeq2i 5024
Description: Equality inference for composition of two classes. (Contributed by NM, 16-Nov-2000.)
Hypothesis
Ref Expression
coeq1i.1  |-  A  =  B
Assertion
Ref Expression
coeq2i  |-  ( C  o.  A )  =  ( C  o.  B
)

Proof of Theorem coeq2i
StepHypRef Expression
1 coeq1i.1 . 2  |-  A  =  B
2 coeq2 5022 . 2  |-  ( A  =  B  ->  ( C  o.  A )  =  ( C  o.  B ) )
31, 2ax-mp 8 1  |-  ( C  o.  A )  =  ( C  o.  B
)
Colors of variables: wff set class
Syntax hints:    = wceq 1652    o. ccom 4873
This theorem is referenced by:  coeq12i  5027  cocnvcnv2  5372  co01  5375  fcoi1  5608  dftpos2  6487  tposco  6501  canthp1  8518  cats1co  11808  imasdsf1olem  18391  evlsval  19928  evl1var  19940  pf1ind  19963  hoico1  23247  hoid1i  23280  pjclem1  23686  pjclem3  23688  pjci  23691  dfpo2  25367  mvdco  27303  cdlemk45  31583
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-in 3319  df-ss 3326  df-br 4205  df-opab 4259  df-co 4878
  Copyright terms: Public domain W3C validator