Definition df-tp 4653

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

Note: ordered triples are a completely different object defined below in df-ot 4657. 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 4652	. 2 class {𝐴, 𝐵, 𝐶}
5	1, 2	cpr 4650	. . 3 class {𝐴, 𝐵}
6	3	csn 4648	. . 3 class {𝐶}
7	5, 6	cun 3974	. 2 class ({𝐴, 𝐵} ∪ {𝐶})
8	4, 7	wceq 1537	1 wff {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})

This definition is referenced by:  eltpg  4709  raltpg  4723  rextpg  4724  disjtpsn  4740  disjtp2  4741  tpeq1  4767  tpeq2  4768  tpeq3  4769  tpcoma  4775  tpass  4777  qdass  4778  tpidm12  4780  diftpsn3  4827  tpprceq3  4829  tppreqb  4830  snsstp1  4841  snsstp2  4842  snsstp3  4843  sstp  4861  tpss  4862  tpssi  4863  ord3ex  5405  dmtpop  6251  funtpg  6635  funtp  6637  fntpg  6640  funcnvtp  6643  fnimatpd  7008  ftpg  7192  fvtp1  7234  fvtp1g  7237  tpex  7783  fr3nr  7809  tpfi  9395  fztp  13642  hashtplei  14535  hashtpg  14536  hash3tpexb  14545  s3tpop  14960  s3rn  15015  sumtp  15799  bpoly3  16108  strle3  17209  estrreslem2  18209  estrres  18210  lsptpcl  21002  perfectlem2  27294  sltsolem1  27740  ex-un  30458  ex-ss  30461  ex-pw  30463  ex-hash  30487  prodtp  32833  gsumtp  33041  dvh4dimlem  41402  dvhdimlem  41403  dvh4dimN  41406  df3o2  43277  df3o3  43278  omcl3g  43298  onsucunitp  43337  oaun3  43346  tr3dom  43492  perfectALTVlem2  47598  isgrtri  47796  usgrexmpl2edg  47846