Definition df-tp 3654

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 3648	. 2 class {𝐴, 𝐵, 𝐶}
5	1, 2	cpr 3647	. . 3 class {𝐴, 𝐵}
6	3	csn 3646	. . 3 class {𝐶}
7	5, 6	cun 3175	. 2 class ({𝐴, 𝐵} ∪ {𝐶})
8	4, 7	wceq 1375	1 wff {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})

This definition is referenced by:  eltpg  3691  raltpg  3699  rextpg  3700  tpeq1  3732  tpeq2  3733  tpeq3  3734  tpcoma  3740  tpass  3742  qdass  3743  tpidm12  3745  diftpsn3  3788  snsstp1  3797  snsstp2  3798  snsstp3  3799  prsstp12  3800  tpss  3815  tpssi  3816  ord3ex  4253  tpexg  4512  dmtpop  5180  funtpg  5348  funtp  5350  fntpg  5353  ftpg  5796  fvtp1g  5820  tpfidisj  7059  tpfidceq  7060  fztp  10242  sumtp  11891  strle3g  13107  lsptpcl  14323  perfectlem2  15639  bdctp  16145