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

Definition df-ot 3625
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 3619 . 2  class  <. A ,  B ,  C >.
51, 2cop 3618 . . 3  class  <. A ,  B >.
65, 3cop 3618 . 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  3780  oteq2  3781  oteq3  3782  otex  4211  otth  4223  fnotovb  5829  ot1stg  6069  ot2ndg  6070  ot3rdg  6071  ottpos  6179  wunot  8314  elhomai2  13830  homadmcd  13838  matval  26834  hdmap1val  31248
  Copyright terms: Public domain W3C validator