ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-ot Structured version   Unicode version

Definition df-ot 3377
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  <. ,  ,  C >. 
<. <. ,  >. ,  C >.

Detailed syntax breakdown of Definition df-ot
StepHypRef Expression
1 cA . . 3
2 cB . . 3
3 cC . . 3  C
41, 2, 3cotp 3371 . 2  <. ,  ,  C >.
51, 2cop 3370 . . 3  <. ,  >.
65, 3cop 3370 . 2  <. <. ,  >. ,  C >.
74, 6wceq 1242 1  <. ,  ,  C >. 
<. <. ,  >. ,  C >.
Colors of variables: wff set class
This definition is referenced by:  oteq1  3549  oteq2  3550  oteq3  3551  otexg  3958  otth  3970  fnotovb  5490  ot1stg  5721  ot2ndg  5722  ot3rdgg  5723  ottposg  5811
  Copyright terms: Public domain W3C validator