Definition df-tp 3744

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

This definition is referenced by:  eltpg  3770  raltpg  3778  rextpg  3779  tpeq1  3809  tpeq2  3810  tpeq3  3811  tpcoma  3817  tpass  3819  qdass  3820  tpidm12  3822  diftpsn3  3850  snsstp1  3859  snsstp2  3860  snsstp3  3861  sstp  3871  tpss  3872  dmtpop  5072  2p1e3c  6157