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	$$⊢\left\{A,B,C\right\}=\left\{A,B\right\}\cup \left\{C\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	$$classA$$
1		cB	$$classB$$
2		cC	$$classC$$
3	0 1 2	ctp	$$class\left\{A,B,C\right\}$$
4	0 1	cpr	$$class\left\{A,B\right\}$$
5	2	csn	$$class\left\{C\right\}$$
6	4 5	cun	$$class\left(\left\{A,B\right\}\cup \left\{C\right\}\right)$$
7	3 6	wceq	$$wff\left\{A,B,C\right\}=\left\{A,B\right\}\cup \left\{C\right\}$$