Definition df-tp 4593

Description: Define unordered triple of classes. Definition of [Enderton] p. 19.

Note: ordered triples are a completely different object defined below in df-ot 4597. As with all tuples, when the term "triple" is used without qualifier, it means "ordered triple". (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 4592	. 2 class {𝐴, 𝐵, 𝐶}
5	1, 2	cpr 4590	. . 3 class {𝐴, 𝐵}
6	3	csn 4588	. . 3 class {𝐶}
7	5, 6	cun 3902	. 2 class ({𝐴, 𝐵} ∪ {𝐶})
8	4, 7	wceq 1568	1 wff {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})

This definition is referenced by:  eltpg  4651  raltpg  4663  rextpg  4664  disjtpsn  4680  disjtp2  4681  tpeq1  4707  tpeq2  4708  tpeq3  4709  tpcoma  4715  tpass  4717  qdass  4718  tpidm12  4720  diftpsn3  4769  tpprceq3  4771  tppreqb  4772  snsstp1  4781  snsstp2  4782  snsstp3  4783  sstp  4800  tpss  4801  tpssi  4802  ord3ex  5358  dmtpop  6219  funtpg  6591  funtp  6593  fntpg  6596  funcnvtp  6599  fnimatpd  6965  ftpg  7153  fvtp1  7193  fvtp1g  7196  tpex  7744  fr3nr  7770  tpfi  9284  fztp  13607  hashtplei  14520  hashtpg  14521  hash3tpexb  14530  s3tpop  14945  s3rn  15000  sumtp  15799  bpoly3  16111  strle3  17219  estrreslem2  18193  estrres  18194  lsptpcl  21079  perfectlem2  27370  ltssolem1  27815  ex-un  30741  ex-ss  30744  ex-pw  30746  ex-hash  30770  tpssg  32849  prodtp  33137  gsumtp  33350  dvh4dimlem  42163  dvhdimlem  42164  dvh4dimN  42167  df3o2  43988  df3o3  43989  omcl3g  44009  onsucunitp  44048  oaun3  44057  tr3dom  44202  perfectALTVlem2  48432  isgrtri  48653  usgrexmpl2edg  48739