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

Definition df-ot 3760
Description: Define ordered triple of classes. Definition of ordered triple in [Stoll] p. 25. (Contributed by NM, 3-Apr-2015.)
Assertion
Ref Expression
df-ot  |-  <. A ,  B ,  C >.  = 
<. <. A ,  B >. ,  C >.

Detailed syntax breakdown of Definition df-ot
StepHypRef Expression
1 cA . . 3  class  A
2 cB . . 3  class  B
3 cC . . 3  class  C
41, 2, 3cotp 3754 . 2  class  <. A ,  B ,  C >.
51, 2cop 3753 . . 3  class  <. A ,  B >.
65, 3cop 3753 . 2  class  <. <. A ,  B >. ,  C >.
74, 6wceq 1649 1  wff  <. A ,  B ,  C >.  = 
<. <. A ,  B >. ,  C >.
Colors of variables: wff set class
This definition is referenced by:  oteq1  3928  oteq2  3929  oteq3  3930  otex  4362  otth  4374  fnotovb  6049  ot1stg  6293  ot2ndg  6294  ot3rdg  6295  ottpos  6418  wunot  8524  elhomai2  14109  homadmcd  14117  fnotaovb  27724  hdmap1val  31965
  Copyright terms: Public domain W3C validator