Definition df-tp 4589

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

Note: ordered triples are a completely different object defined below in df-ot 4593. 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 4588	. 2 class {𝐴, 𝐵, 𝐶}
5	1, 2	cpr 4586	. . 3 class {𝐴, 𝐵}
6	3	csn 4584	. . 3 class {𝐶}
7	5, 6	cun 3904	. 2 class ({𝐴, 𝐵} ∪ {𝐶})
8	4, 7	wceq 1562	1 wff {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})

This definition is referenced by:  eltpg  4647  raltpg  4659  rextpg  4660  disjtpsn  4676  disjtp2  4677  tpeq1  4703  tpeq2  4704  tpeq3  4705  tpcoma  4711  tpass  4713  qdass  4714  tpidm12  4716  diftpsn3  4764  tpprceq3  4766  tppreqb  4767  snsstp1  4776  snsstp2  4777  snsstp3  4778  sstp  4796  tpss  4797  tpssi  4798  ord3ex  5346  dmtpop  6207  funtpg  6578  funtp  6580  fntpg  6583  funcnvtp  6586  fnimatpd  6953  ftpg  7141  fvtp1  7181  fvtp1g  7184  tpex  7731  fr3nr  7757  tpfi  9272  fztp  13587  hashtplei  14499  hashtpg  14500  hash3tpexb  14509  s3tpop  14924  s3rn  14979  sumtp  15778  bpoly3  16090  strle3  17198  estrreslem2  18172  estrres  18173  lsptpcl  21048  perfectlem2  27296  ltssolem1  27741  ex-un  30628  ex-ss  30631  ex-pw  30633  ex-hash  30657  tpssg  32738  prodtp  33031  gsumtp  33246  dvh4dimlem  42072  dvhdimlem  42073  dvh4dimN  42076  df3o2  43895  df3o3  43896  omcl3g  43916  onsucunitp  43955  oaun3  43964  tr3dom  44109  perfectALTVlem2  48349  isgrtri  48570  usgrexmpl2edg  48656