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

Theorem coeq2i 4974
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 4972 . 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 1649    o. ccom 4823
This theorem is referenced by:  coeq12i  4977  cocnvcnv2  5322  co01  5325  fcoi1  5558  dftpos2  6433  tposco  6447  canthp1  8463  cats1co  11748  imasdsf1olem  18312  evlsval  19808  evl1var  19820  pf1ind  19843  hoico1  23108  hoid1i  23141  pjclem1  23547  pjclem3  23549  pjci  23552  dfpo2  25137  mvdco  27058  cdlemk45  31062
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2369
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2375  df-cleq 2381  df-clel 2384  df-nfc 2513  df-in 3271  df-ss 3278  df-br 4155  df-opab 4209  df-co 4828
  Copyright terms: Public domain W3C validator