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 1569	1 wff {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})

This definition is used 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  5357  dmtpop  6218  funtpg  6591  funtp  6593  fntpg  6596  funcnvtp  6599  fnimatpd  6965  ftpg  7153  fvtp1  7193  fvtp1g  7196  tpex  7745  fr3nr  7769  tpfi  9283  fztp  13615  hashtplei  14528  hashtpg  14529  hash3tpexb  14538  s3tpop  14953  s3rn  15008  sumtp  15807  bpoly3  16118  strle3  17226  estrreslem2  18200  estrres  18201  lsptpcl  21111  perfectlem2  27405  ltssolem1  27850  ex-un  30786  ex-ss  30789  ex-pw  30791  ex-hash  30815  tpssg  32894  prodtp  33182  gsumtp  33393  dvh4dimlem  42245  dvhdimlem  42246  dvh4dimN  42249  df3o2  44068  df3o3  44069  omcl3g  44089  onsucunitp  44128  oaun3  44137  tr3dom  44282  perfectALTVlem2  48515  isgrtri  48736  usgrexmpl2edg  48822