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

Definition df-ot 3663
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 3657 . 2  class  <. A ,  B ,  C >.
51, 2cop 3656 . . 3  class  <. A ,  B >.
65, 3cop 3656 . 2  class  <. <. A ,  B >. ,  C >.
74, 6wceq 1632 1  wff  <. A ,  B ,  C >.  = 
<. <. A ,  B >. ,  C >.
Colors of variables: wff set class
This definition is referenced by:  oteq1  3821  oteq2  3822  oteq3  3823  otex  4254  otth  4266  fnotovb  5910  ot1stg  6150  ot2ndg  6151  ot3rdg  6152  ottpos  6260  wunot  8361  elhomai2  13882  homadmcd  13890  matval  27568  fnotaovb  28166  hdmap1val  32611
  Copyright terms: Public domain W3C validator