Definition df-tp 4562

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

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

This definition is referenced by:  eltpg  4620  raltpg  4632  rextpg  4633  disjtpsn  4649  disjtp2  4650  tpeq1  4676  tpeq2  4677  tpeq3  4678  tpcoma  4684  tpass  4686  qdass  4687  tpidm12  4689  diftpsn3  4737  tpprceq3  4739  tppreqb  4740  snsstp1  4749  snsstp2  4750  snsstp3  4751  sstp  4769  tpss  4770  tpssi  4771  ord3ex  5318  dmtpop  6171  funtpg  6542  funtp  6544  fntpg  6547  funcnvtp  6550  fnimatpd  6913  ftpg  7099  fvtp1  7139  fvtp1g  7142  tpex  7689  fr3nr  7715  tpfi  9225  fztp  13523  hashtplei  14435  hashtpg  14436  hash3tpexb  14445  s3tpop  14860  s3rn  14915  sumtp  15700  bpoly3  16012  strle3  17119  estrreslem2  18093  estrres  18094  lsptpcl  20963  perfectlem2  27181  ltssolem1  27627  ex-un  30482  ex-ss  30485  ex-pw  30487  ex-hash  30511  tpssg  32595  prodtp  32888  gsumtp  33113  dvh4dimlem  41877  dvhdimlem  41878  dvh4dimN  41881  df3o2  43729  df3o3  43730  omcl3g  43750  onsucunitp  43789  oaun3  43798  tr3dom  43943  perfectALTVlem2  48186  isgrtri  48407  usgrexmpl2edg  48493