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 4149	. 2 class ({𝐴, 𝐵} ∪ {𝐶})
8	4, 7	wceq 1569	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  6219  funtpg  6595  funtp  6597  fntpg  6600  funcnvtp  6603  fnimatpd  6969  xpsntpg  7144  ftpg  7160  fvtp1  7200  fvtp1g  7203  tpex  7762  fr3nr  7786  tpfi  9317  fztp  13714  hashtplei  14629  hashtpg  14630  hash3tpexb  14639  s3tpop  15060  s3rn  15117  sumtp  15915  bpoly3  16224  strle3  17338  estrreslem2  18312  estrres  18313  lsptpcl  21254  perfectlem2  27557  ltssolem1  28032  ex-un  31025  ex-ss  31028  ex-pw  31030  ex-hash  31054  tpssg  33175  prodtp  33460  gsumtp  33667  dvh4dimlem  42543  dvhdimlem  42544  dvh4dimN  42547  df3o2  44357  df3o3  44358  omcl3g  44378  onsucunitp  44417  oaun3  44426  tr3dom  44571  perfectALTVlem2  48862  isgrtri  49083  usgrexmpl2edg  49169