Users' Mathboxes Mathbox for Frédéric Liné < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-cmpa Unicode version

Definition df-cmpa 25720
Description: Definition of  o_. (Contributed by FL, 26-Oct-2007.)
Assertion
Ref Expression
df-cmpa  |-  o_  =  ( 2nd  o.  2nd )

Detailed syntax breakdown of Definition df-cmpa
StepHypRef Expression
1 co_ 25715 . 2  class  o_
2 c2nd 6121 . . 3  class  2nd
32, 2ccom 4693 . 2  class  ( 2nd 
o.  2nd )
41, 3wceq 1623 1  wff  o_  =  ( 2nd  o.  2nd )
Colors of variables: wff set class
This definition is referenced by:  cmpval  25726
  Copyright terms: Public domain W3C validator