Definition df-tp 4588

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

Note: ordered triples are a completely different object defined below in df-ot 4592. 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 4587	. 2 class {𝐴, 𝐵, 𝐶}
5	1, 2	cpr 4585	. . 3 class {𝐴, 𝐵}
6	3	csn 4583	. . 3 class {𝐶}
7	5, 6	cun 3896	. 2 class ({𝐴, 𝐵} ∪ {𝐶})
8	4, 7	wceq 1570	1 wff {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})

This definition is used by:  eltpg  4646  raltpg  4658  rextpg  4659  disjtpsn  4675  disjtp2  4676  tpeq1  4702  tpeq2  4703  tpeq3  4704  tpcoma  4710  tpass  4712  qdass  4713  tpidm12  4715  diftpsn3  4764  tpprceq3  4766  tppreqb  4767  snsstp1  4776  snsstp2  4777  snsstp3  4778  sstp  4795  tpss  4796  tpssi  4797  ord3ex  5348  dmtpop  6208  funtpg  6583  funtp  6585  fntpg  6588  funcnvtp  6591  fnimatpd  6957  xpsntpg  7132  ftpg  7148  fvtp1  7188  fvtp1g  7191  tpex  7745  fr3nr  7769  tpfi  9295  fztp  13682  hashtplei  14596  hashtpg  14597  hash3tpexb  14606  s3tpop  15027  s3rn  15084  sumtp  15882  bpoly3  16191  strle3  17299  estrreslem2  18273  estrres  18274  lsptpcl  21215  perfectlem2  27520  ltssolem1  27965  ex-un  30958  ex-ss  30961  ex-pw  30963  ex-hash  30987  tpssg  33066  prodtp  33351  gsumtp  33558  dvh4dimlem  42420  dvhdimlem  42421  dvh4dimN  42424  df3o2  44258  df3o3  44259  omcl3g  44279  onsucunitp  44318  oaun3  44327  tr3dom  44472  perfectALTVlem2  48742  isgrtri  48963  usgrexmpl2edg  49049