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

Definition df-ot 3826
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 3820 . 2  class  <. A ,  B ,  C >.
51, 2cop 3819 . . 3  class  <. A ,  B >.
65, 3cop 3819 . 2  class  <. <. A ,  B >. ,  C >.
74, 6wceq 1653 1  wff  <. A ,  B ,  C >.  = 
<. <. A ,  B >. ,  C >.
Colors of variables: wff set class
This definition is referenced by:  oteq1  3995  oteq2  3996  oteq3  3997  otex  4431  otth  4443  fnotovb  6120  ot1stg  6364  ot2ndg  6365  ot3rdg  6366  ottpos  6492  wunot  8603  elhomai2  14194  homadmcd  14202  fnotaovb  28052  el2xptp  28075  el2xptp0  28076  otel3xp  28077  otthg  28079  el2wlkonotot0  28404  2wlkonotv  28409  hdmap1val  32671
  Copyright terms: Public domain W3C validator