Definition df-tp 3631

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

This definition is referenced by:  eltpg  3668  raltpg  3676  rextpg  3677  tpeq1  3709  tpeq2  3710  tpeq3  3711  tpcoma  3717  tpass  3719  qdass  3720  tpidm12  3722  diftpsn3  3764  snsstp1  3773  snsstp2  3774  snsstp3  3775  prsstp12  3776  tpss  3789  tpssi  3790  ord3ex  4224  tpexg  4480  dmtpop  5146  funtpg  5310  funtp  5312  fntpg  5315  ftpg  5749  fvtp1g  5773  tpfidisj  6999  tpfidceq  7000  fztp  10170  sumtp  11596  strle3g  12811  lsptpcl  14026  perfectlem2  15320  bdctp  15602