Definition df-tp 3626

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 3620	. 2 class {𝐴, 𝐵, 𝐶}
5	1, 2	cpr 3619	. . 3 class {𝐴, 𝐵}
6	3	csn 3618	. . 3 class {𝐶}
7	5, 6	cun 3151	. 2 class ({𝐴, 𝐵} ∪ {𝐶})
8	4, 7	wceq 1364	1 wff {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})

This definition is referenced by:  eltpg  3663  raltpg  3671  rextpg  3672  tpeq1  3704  tpeq2  3705  tpeq3  3706  tpcoma  3712  tpass  3714  qdass  3715  tpidm12  3717  diftpsn3  3759  snsstp1  3768  snsstp2  3769  snsstp3  3770  prsstp12  3771  tpss  3784  tpssi  3785  ord3ex  4219  tpexg  4475  dmtpop  5141  funtpg  5305  funtp  5307  fntpg  5310  ftpg  5742  fvtp1g  5766  tpfidisj  6984  fztp  10144  sumtp  11557  strle3g  12726  lsptpcl  13890  bdctp  15364