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

Definition df-ot 3816
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 3810 . 2  class  <. A ,  B ,  C >.
51, 2cop 3809 . . 3  class  <. A ,  B >.
65, 3cop 3809 . 2  class  <. <. A ,  B >. ,  C >.
74, 6wceq 1652 1  wff  <. A ,  B ,  C >.  = 
<. <. A ,  B >. ,  C >.
Colors of variables: wff set class
This definition is referenced by:  oteq1  3985  oteq2  3986  oteq3  3987  otex  4420  otth  4432  fnotovb  6109  ot1stg  6353  ot2ndg  6354  ot3rdg  6355  ottpos  6481  wunot  8590  elhomai2  14181  homadmcd  14189  fnotaovb  28029  el2xptp  28050  el2xptp0  28051  otel3xp  28052  otthg  28054  el2wlkonotot0  28292  2wlkonotv  28297  hdmap1val  32534
  Copyright terms: Public domain W3C validator