Definition df-tp 3584

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 3578	. 2 class {𝐴, 𝐵, 𝐶}
5	1, 2	cpr 3577	. . 3 class {𝐴, 𝐵}
6	3	csn 3576	. . 3 class {𝐶}
7	5, 6	cun 3114	. 2 class ({𝐴, 𝐵} ∪ {𝐶})
8	4, 7	wceq 1343	1 wff {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})

This definition is referenced by:  eltpg  3621  raltpg  3629  rextpg  3630  tpeq1  3662  tpeq2  3663  tpeq3  3664  tpcoma  3670  tpass  3672  qdass  3673  tpidm12  3675  diftpsn3  3714  snsstp1  3723  snsstp2  3724  snsstp3  3725  prsstp12  3726  tpss  3738  tpssi  3739  ord3ex  4169  tpexg  4422  dmtpop  5079  funtpg  5239  funtp  5241  fntpg  5244  ftpg  5669  fvtp1g  5693  tpfidisj  6893  fztp  10013  sumtp  11355  strle3g  12487  bdctp  13754