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	⊢ { 𝐴 , 𝐵 , 𝐶 } = ( { 𝐴 , 𝐵 } ∪ { 𝐶 } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	⊢ 𝐴
1		cB	⊢ 𝐵
2		cC	⊢ 𝐶
3	0 1 2	ctp	⊢ { 𝐴 , 𝐵 , 𝐶 }
4	0 1	cpr	⊢ { 𝐴 , 𝐵 }
5	2	csn	⊢ { 𝐶 }
6	4 5	cun	⊢ ( { 𝐴 , 𝐵 } ∪ { 𝐶 } )
7	3 6	wceq	⊢ { 𝐴 , 𝐵 , 𝐶 } = ( { 𝐴 , 𝐵 } ∪ { 𝐶 } )