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	$$classA$$
1		cB	$$classB$$
2		cC	$$classC$$
3	0 1 2	cotp	$$class⟨A,B,C⟩$$
4	0 1	cop	$$class⟨A,B⟩$$
5	4 2	cop	$$class⟨⟨A,B⟩,C⟩$$
6	3 5	wceq	$$wff⟨A,B,C⟩=⟨⟨A,B⟩,C⟩$$