Definition df-tp 3642

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 3636	. 2 class {𝐴, 𝐵, 𝐶}
5	1, 2	cpr 3635	. . 3 class {𝐴, 𝐵}
6	3	csn 3634	. . 3 class {𝐶}
7	5, 6	cun 3165	. 2 class ({𝐴, 𝐵} ∪ {𝐶})
8	4, 7	wceq 1373	1 wff {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})

This definition is referenced by:  eltpg  3679  raltpg  3687  rextpg  3688  tpeq1  3720  tpeq2  3721  tpeq3  3722  tpcoma  3728  tpass  3730  qdass  3731  tpidm12  3733  diftpsn3  3776  snsstp1  3785  snsstp2  3786  snsstp3  3787  prsstp12  3788  tpss  3801  tpssi  3802  ord3ex  4238  tpexg  4495  dmtpop  5163  funtpg  5330  funtp  5332  fntpg  5335  ftpg  5775  fvtp1g  5799  tpfidisj  7033  tpfidceq  7034  fztp  10207  sumtp  11769  strle3g  12984  lsptpcl  14200  perfectlem2  15516  bdctp  15882