Definition df-tp 3601

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 3595	. 2 class {𝐴, 𝐵, 𝐶}
5	1, 2	cpr 3594	. . 3 class {𝐴, 𝐵}
6	3	csn 3593	. . 3 class {𝐶}
7	5, 6	cun 3128	. 2 class ({𝐴, 𝐵} ∪ {𝐶})
8	4, 7	wceq 1353	1 wff {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})

This definition is referenced by:  eltpg  3638  raltpg  3646  rextpg  3647  tpeq1  3679  tpeq2  3680  tpeq3  3681  tpcoma  3687  tpass  3689  qdass  3690  tpidm12  3692  diftpsn3  3734  snsstp1  3743  snsstp2  3744  snsstp3  3745  prsstp12  3746  tpss  3759  tpssi  3760  ord3ex  4191  tpexg  4445  dmtpop  5105  funtpg  5268  funtp  5270  fntpg  5273  ftpg  5701  fvtp1g  5725  tpfidisj  6927  fztp  10078  sumtp  11422  strle3g  12567  bdctp  14627