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

Definition df-ot 3651
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 3645 . 2  class  <. A ,  B ,  C >.
51, 2cop 3644 . . 3  class  <. A ,  B >.
65, 3cop 3644 . 2  class  <. <. A ,  B >. ,  C >.
74, 6wceq 1623 1  wff  <. A ,  B ,  C >.  = 
<. <. A ,  B >. ,  C >.
Colors of variables: wff set class
This definition is referenced by:  oteq1  3806  oteq2  3807  oteq3  3808  otex  4237  otth  4249  fnotovb  5856  ot1stg  6096  ot2ndg  6097  ot3rdg  6098  ottpos  6206  wunot  8341  elhomai2  13862  homadmcd  13870  matval  26876  fnotaovb  27449  hdmap1val  31268
  Copyright terms: Public domain W3C validator