Metamath Proof Explorer

Definition df-ot

Description: Define ordered triple of classes. Definition of ordered triple in Stoll p. 25. (Contributed by NM, 3-Apr-2015)

Ref Expression
Assertion df-ot 
|- <. A , B , C >. = <. <. A , B >. , C >.

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA 
 |-  A
1 cB 
 |-  B
2 cC 
 |-  C
3 0 1 2 cotp 
 |-  <. A , B , C >.
4 0 1 cop 
 |-  <. A , B >.
5 4 2 cop 
 |-  <. <. A , B >. , C >.
6 3 5 wceq 
 |-  <. A , B , C >. = <. <. A , B >. , C >.