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	⊢ ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ = ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 ⟩

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	⊢ 𝐴
1		cB	⊢ 𝐵
2		cC	⊢ 𝐶
3	0 1 2	cotp	⊢ ⟨ 𝐴 , 𝐵 , 𝐶 ⟩
4	0 1	cop	⊢ ⟨ 𝐴 , 𝐵 ⟩
5	4 2	cop	⊢ ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 ⟩
6	3 5	wceq	⊢ ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ = ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 ⟩