Definition df-tp 3627

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

This definition is referenced by:  eltpg  3664  raltpg  3672  rextpg  3673  tpeq1  3705  tpeq2  3706  tpeq3  3707  tpcoma  3713  tpass  3715  qdass  3716  tpidm12  3718  diftpsn3  3760  snsstp1  3769  snsstp2  3770  snsstp3  3771  prsstp12  3772  tpss  3785  tpssi  3786  ord3ex  4220  tpexg  4476  dmtpop  5142  funtpg  5306  funtp  5308  fntpg  5311  ftpg  5743  fvtp1g  5767  tpfidisj  6986  fztp  10147  sumtp  11560  strle3g  12729  lsptpcl  13893  bdctp  15434