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

Definition df-ot 3784
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 3778 . 2  class  <. A ,  B ,  C >.
51, 2cop 3777 . . 3  class  <. A ,  B >.
65, 3cop 3777 . 2  class  <. <. A ,  B >. ,  C >.
74, 6wceq 1649 1  wff  <. A ,  B ,  C >.  = 
<. <. A ,  B >. ,  C >.
Colors of variables: wff set class
This definition is referenced by:  oteq1  3953  oteq2  3954  oteq3  3955  otex  4388  otth  4400  fnotovb  6076  ot1stg  6320  ot2ndg  6321  ot3rdg  6322  ottpos  6448  wunot  8554  elhomai2  14144  homadmcd  14152  fnotaovb  27929  el2xptp  27948  el2xptp0  27949  otel3xp  27950  otthg  27952  el2wlkonotot0  28069  2wlkonotv  28074  hdmap1val  32282
  Copyright terms: Public domain W3C validator