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

Definition df-ot 3591
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 3585 . 2  class  <. A ,  B ,  C >.
51, 2cop 3584 . . 3  class  <. A ,  B >.
65, 3cop 3584 . 2  class  <. <. A ,  B >. ,  C >.
74, 6wceq 1619 1  wff  <. A ,  B ,  C >.  = 
<. <. A ,  B >. ,  C >.
Colors of variables: wff set class
This definition is referenced by:  oteq1  3746  oteq2  3747  oteq3  3748  otex  4175  otth  4187  fnotovb  5793  ot1stg  6033  ot2ndg  6034  ot3rdg  6035  ottpos  6143  wunot  8278  elhomai2  13793  homadmcd  13801  matval  26797  hdmap1val  31119
  Copyright terms: Public domain W3C validator