Definition df-tp 3600

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

This definition is referenced by:  eltpg  3637  raltpg  3645  rextpg  3646  tpeq1  3678  tpeq2  3679  tpeq3  3680  tpcoma  3686  tpass  3688  qdass  3689  tpidm12  3691  diftpsn3  3733  snsstp1  3742  snsstp2  3743  snsstp3  3744  prsstp12  3745  tpss  3758  tpssi  3759  ord3ex  4190  tpexg  4444  dmtpop  5104  funtpg  5267  funtp  5269  fntpg  5272  ftpg  5700  fvtp1g  5724  tpfidisj  6926  fztp  10077  sumtp  11421  strle3g  12566  bdctp  14594