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

Definition df-ot 3610
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 3604 . 2  class  <. A ,  B ,  C >.
51, 2cop 3603 . . 3  class  <. A ,  B >.
65, 3cop 3603 . 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  3765  oteq2  3766  oteq3  3767  otex  4196  otth  4208  fnotovb  5814  ot1stg  6054  ot2ndg  6055  ot3rdg  6056  ottpos  6164  wunot  8299  elhomai2  13814  homadmcd  13822  matval  26818  hdmap1val  31140
  Copyright terms: Public domain W3C validator