Definition df-tp 4632

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

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

This definition is referenced by:  eltpg  4688  raltpg  4701  rextpg  4702  disjtpsn  4718  disjtp2  4719  tpeq1  4745  tpeq2  4746  tpeq3  4747  tpcoma  4753  tpass  4755  qdass  4756  tpidm12  4758  diftpsn3  4804  tpprceq3  4806  tppreqb  4807  snsstp1  4818  snsstp2  4819  snsstp3  4820  sstp  4836  tpss  4837  tpssi  4838  ord3ex  5384  dmtpop  6214  funtpg  6600  funtp  6602  fntpg  6605  funcnvtp  6608  ftpg  7149  fvtp1  7191  fvtp1g  7194  tpex  7729  fr3nr  7754  tpfi  9319  fztp  13553  hashtplei  14441  hashtpg  14442  s3tpop  14856  sumtp  15691  bpoly3  15998  strle3  17089  estrreslem2  18086  estrres  18087  lsptpcl  20578  perfectlem2  26713  sltsolem1  27158  ex-un  29657  ex-ss  29660  ex-pw  29662  ex-hash  29686  fnimatp  31880  prodtp  32011  dvh4dimlem  40252  dvhdimlem  40253  dvh4dimN  40256  df3o2  41996  df3o3  41997  omcl3g  42017  onsucunitp  42056  oaun3  42065  tr3dom  42212  perfectALTVlem2  46325