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

Definition df-ot 3650
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 3644 . 2  class  <. A ,  B ,  C >.
51, 2cop 3643 . . 3  class  <. A ,  B >.
65, 3cop 3643 . 2  class  <. <. A ,  B >. ,  C >.
74, 6wceq 1623 1  wff  <. A ,  B ,  C >.  = 
<. <. A ,  B >. ,  C >.
Colors of variables: wff set class
This definition is referenced by:  oteq1  3805  oteq2  3806  oteq3  3807  otex  4238  otth  4250  fnotovb  5894  ot1stg  6134  ot2ndg  6135  ot3rdg  6136  ottpos  6244  wunot  8345  elhomai2  13866  homadmcd  13874  matval  27465  fnotaovb  28058  hdmap1val  31989
  Copyright terms: Public domain W3C validator