Definition df-tp 3743

Description: Define unordered triple of classes. Definition of [Enderton] p. 19. (Contributed by NM, 9-Apr-1994.)

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 3739	. 2 class {A, B, C}
5	1, 2	cpr 3738	. . 3 class {A, B}
6	3	csn 3737	. . 3 class {C}
7	5, 6	cun 3207	. 2 class ({A, B} ∪ {C})
8	4, 7	wceq 1642	1 wff {A, B, C} = ({A, B} ∪ {C})

This definition is referenced by:  eltpg  3769  raltpg  3777  rextpg  3778  tpeq1  3808  tpeq2  3809  tpeq3  3810  tpcoma  3816  tpass  3818  qdass  3819  tpidm12  3821  diftpsn3  3849  snsstp1  3858  snsstp2  3859  snsstp3  3860  sstp  3870  tpss  3871  dmtpop  5071  2p1e3c  6156