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

Definition df-ot 3652
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 3646 . 2  class  <. A ,  B ,  C >.
51, 2cop 3645 . . 3  class  <. A ,  B >.
65, 3cop 3645 . 2  class  <. <. A ,  B >. ,  C >.
74, 6wceq 1625 1  wff  <. A ,  B ,  C >.  = 
<. <. A ,  B >. ,  C >.
Colors of variables: wff set class
This definition is referenced by:  oteq1  3807  oteq2  3808  oteq3  3809  otex  4240  otth  4252  fnotovb  5896  ot1stg  6136  ot2ndg  6137  ot3rdg  6138  ottpos  6246  wunot  8347  elhomai2  13868  homadmcd  13876  matval  27476  fnotaovb  28069  hdmap1val  32062
  Copyright terms: Public domain W3C validator