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

Definition df-ot 3726
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 3720 . 2  class  <. A ,  B ,  C >.
51, 2cop 3719 . . 3  class  <. A ,  B >.
65, 3cop 3719 . 2  class  <. <. A ,  B >. ,  C >.
74, 6wceq 1642 1  wff  <. A ,  B ,  C >.  = 
<. <. A ,  B >. ,  C >.
Colors of variables: wff set class
This definition is referenced by:  oteq1  3886  oteq2  3887  oteq3  3888  otex  4320  otth  4332  fnotovb  5981  ot1stg  6221  ot2ndg  6222  ot3rdg  6223  ottpos  6331  wunot  8435  elhomai2  13965  homadmcd  13973  matval  26788  fnotaovb  27386  hdmap1val  32058
  Copyright terms: Public domain W3C validator