Definition df-tp 4587

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

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

This definition is referenced by:  eltpg  4645  raltpg  4657  rextpg  4658  disjtpsn  4674  disjtp2  4675  tpeq1  4701  tpeq2  4702  tpeq3  4703  tpcoma  4709  tpass  4711  qdass  4712  tpidm12  4714  diftpsn3  4760  tpprceq3  4762  tppreqb  4763  snsstp1  4774  snsstp2  4775  snsstp3  4776  sstp  4794  tpss  4795  tpssi  4796  ord3ex  5336  dmtpop  6186  funtpg  6557  funtp  6559  fntpg  6562  funcnvtp  6565  fnimatpd  6928  ftpg  7113  fvtp1  7153  fvtp1g  7156  tpex  7703  fr3nr  7729  tpfi  9240  fztp  13510  hashtplei  14421  hashtpg  14422  hash3tpexb  14431  s3tpop  14846  s3rn  14901  sumtp  15686  bpoly3  15995  strle3  17101  estrreslem2  18075  estrres  18076  lsptpcl  20947  perfectlem2  27214  ltssolem1  27660  ex-un  30517  ex-ss  30520  ex-pw  30522  ex-hash  30546  tpssg  32630  prodtp  32925  gsumtp  33164  dvh4dimlem  41848  dvhdimlem  41849  dvh4dimN  41852  df3o2  43699  df3o3  43700  omcl3g  43720  onsucunitp  43759  oaun3  43768  tr3dom  43913  perfectALTVlem2  48111  isgrtri  48332  usgrexmpl2edg  48418