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

Theorem coeq2i 5101
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 5099 . 2  |-  ( A  =  B  ->  ( C  o.  A )  =  ( C  o.  B ) )
31, 2ax-mp 5 1  |-  ( C  o.  A )  =  ( C  o.  B
)
Colors of variables: wff setvar class
Syntax hints:    = wceq 1370    o. ccom 4945
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-in 3436  df-ss 3443  df-br 4394  df-opab 4452  df-co 4950
This theorem is referenced by:  coeq12i  5104  cocnvcnv2  5450  co01  5453  fcoi1  5686  dftpos2  6865  tposco  6879  canthp1  8925  cats1co  12594  mvdco  16062  evlsval  17721  evl1fval1lem  17882  evl1var  17888  pf1ind  17907  imasdsf1olem  20073  hoico1  25305  hoid1i  25338  pjclem1  25744  pjclem3  25746  pjci  25749  dfpo2  27702  cdlemk45  34900
  Copyright terms: Public domain W3C validator