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

Definition df-ot 3554
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 3548 . 2  class  <. A ,  B ,  C >.
51, 2cop 3547 . . 3  class  <. A ,  B >.
65, 3cop 3547 . 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  3705  oteq2  3706  oteq3  3707  otex  4131  otth  4143  fnotovb  5746  ot1stg  5986  ot2ndg  5987  ot3rdg  5988  ottpos  6096  wunot  8225  elhomai2  13710  homadmcd  13718  matval  26631  hdmap1val  30678
  Copyright terms: Public domain W3C validator