Definition df-tp 4382

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 4381	. 2 class {𝐴, 𝐵, 𝐶}
5	1, 2	cpr 4379	. . 3 class {𝐴, 𝐵}
6	3	csn 4377	. . 3 class {𝐶}
7	5, 6	cun 3774	. 2 class ({𝐴, 𝐵} ∪ {𝐶})
8	4, 7	wceq 1637	1 wff {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})

This definition is referenced by:  eltpg  4426  raltpg  4435  rextpg  4436  disjtpsn  4449  disjtp2  4450  tpeq1  4475  tpeq2  4476  tpeq3  4477  tpcoma  4483  tpass  4485  qdass  4486  tpidm12  4488  diftpsn3  4530  tpprceq3  4532  tppreqb  4533  snsstp1  4544  snsstp2  4545  snsstp3  4546  sstp  4562  tpss  4563  tpssi  4564  ord3ex  5063  dmtpop  5830  funtpg  6158  funtp  6160  fntpg  6163  funcnvtp  6166  ftpg  6650  fvtp1  6688  fvtp1g  6691  tpex  7190  fr3nr  7212  tpfi  8478  fztp  12623  hashtplei  13486  hashtpg  13487  s3tpop  13881  sumtp  14704  bpoly3  15012  strlemor3OLD  16185  strle3  16189  estrreslem2  16985  estrresOLD  16986  estrres  16987  lsptpcl  19189  perfectlem2  25175  ex-un  27618  ex-ss  27621  ex-pw  27623  ex-hash  27647  prodtp  29906  sltsolem1  32152  dvh4dimlem  37225  dvhdimlem  37226  dvh4dimN  37229  df3o2  38823  df3o3  38824  perfectALTVlem2  42207