Definition df-tp

Description: Define unordered triple of classes. Definition of Enderton p. 19. (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	⊢ { 𝐴 , 𝐵 , 𝐶 } = ( { 𝐴 , 𝐵 } ∪ { 𝐶 } )