Definition df-tp 3482

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 3476	. 2 class {𝐴, 𝐵, 𝐶}
5	1, 2	cpr 3475	. . 3 class {𝐴, 𝐵}
6	3	csn 3474	. . 3 class {𝐶}
7	5, 6	cun 3019	. 2 class ({𝐴, 𝐵} ∪ {𝐶})
8	4, 7	wceq 1299	1 wff {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})

This definition is referenced by:  eltpg  3516  raltpg  3523  rextpg  3524  tpeq1  3556  tpeq2  3557  tpeq3  3558  tpcoma  3564  tpass  3566  qdass  3567  tpidm12  3569  diftpsn3  3608  snsstp1  3617  snsstp2  3618  snsstp3  3619  prsstp12  3620  tpss  3632  tpssi  3633  ord3ex  4054  tpexg  4303  dmtpop  4950  funtpg  5110  funtp  5112  fntpg  5115  ftpg  5536  fvtp1g  5560  tpfidisj  6745  fztp  9699  sumtp  11022  strle3g  11833  bdctp  12651