Definition df-tp 2473

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

Assertion

Ref	Expression
df-tp	⊢ {A, B, C} = ({A, B} ∪ {C})

Detailed syntax breakdown of Definition df-tp

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cB	. . 3 class B
3		cC	. . 3 class C
4	1, 2, 3	ctp 2472	. 2 class {A, B, C}
5	1, 2	cpr 2468	. . 3 class {A, B}
6	3	csn 2467	. . 3 class {C}
7	5, 6	cun 2097	. 2 class ({A, B} ∪ {C})
8	4, 7	wceq 992	1 wff {A, B, C} = ({A, B} ∪ {C})

This definition is referenced by:  eltp 2500  tpi1 2518  tpi2 2519  tpi3 2520  ord3ex 2830  tpex 3102

Copyright terms: Public domain