Definition df-tp 3612

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

Assertion

Ref	Expression
df-tp	⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})

Detailed syntax breakdown of Definition df-tp

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cB	. . 3 class 𝐵
3		cC	. . 3 class 𝐶
4	1, 2, 3	ctp 3606	. 2 class {𝐴, 𝐵, 𝐶}
5	1, 2	cpr 3605	. . 3 class {𝐴, 𝐵}
6	3	csn 3604	. . 3 class {𝐶}
7	5, 6	cun 3139	. 2 class ({𝐴, 𝐵} ∪ {𝐶})
8	4, 7	wceq 1363	1 wff {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})

This definition is referenced by:  eltpg  3649  raltpg  3657  rextpg  3658  tpeq1  3690  tpeq2  3691  tpeq3  3692  tpcoma  3698  tpass  3700  qdass  3701  tpidm12  3703  diftpsn3  3745  snsstp1  3754  snsstp2  3755  snsstp3  3756  prsstp12  3757  tpss  3770  tpssi  3771  ord3ex  4202  tpexg  4456  dmtpop  5116  funtpg  5279  funtp  5281  fntpg  5284  ftpg  5713  fvtp1g  5737  tpfidisj  6941  fztp  10092  sumtp  11436  strle3g  12582  lsptpcl  13583  bdctp  14920