Definition df-tp

Description: Define unordered triple of classes. Definition of Enderton p. 19.

Note: ordered triples are a completely different object defined below in df-ot . As with all tuples, when the term "triple" is used without qualifier, it means "ordered triple". (Contributed by NM, 9-Apr-1994)

	Ref	Expression
Assertion	df-tp	|- { A , B , C } = ( { A , B } u. { C } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	|- A
1		cB	|- B
2		cC	|- C
3	0 1 2	ctp	|- { A , B , C }
4	0 1	cpr	|- { A , B }
5	2	csn	|- { C }
6	4 5	cun	|- ( { A , B } u. { C } )
7	3 6	wceq	|- { A , B , C } = ( { A , B } u. { C } )