This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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⟩$

Step	Hyp	Ref	Expression
0		cA	$class A$
1		cB	$class B$
2		cC	$class C$
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⟩$