Definition df-tp 3630

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

This definition is referenced by:  eltpg  3667  raltpg  3675  rextpg  3676  tpeq1  3708  tpeq2  3709  tpeq3  3710  tpcoma  3716  tpass  3718  qdass  3719  tpidm12  3721  diftpsn3  3763  snsstp1  3772  snsstp2  3773  snsstp3  3774  prsstp12  3775  tpss  3788  tpssi  3789  ord3ex  4223  tpexg  4479  dmtpop  5145  funtpg  5309  funtp  5311  fntpg  5314  ftpg  5746  fvtp1g  5770  tpfidisj  6990  tpfidceq  6991  fztp  10153  sumtp  11579  strle3g  12786  lsptpcl  13950  perfectlem2  15236  bdctp  15518