Definition df-tp 4572

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

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

This definition is referenced by:  eltpg  4627  raltpg  4640  rextpg  4641  disjtpsn  4657  disjtp2  4658  tpeq1  4684  tpeq2  4685  tpeq3  4686  tpcoma  4692  tpass  4694  qdass  4695  tpidm12  4697  diftpsn3  4741  tpprceq3  4743  tppreqb  4744  snsstp1  4755  snsstp2  4756  snsstp3  4757  sstp  4773  tpss  4774  tpssi  4775  ord3ex  5314  dmtpop  6120  funtpg  6487  funtp  6489  fntpg  6492  funcnvtp  6495  ftpg  7025  fvtp1  7067  fvtp1g  7070  tpex  7591  fr3nr  7616  tpfi  9068  fztp  13311  hashtplei  14196  hashtpg  14197  s3tpop  14620  sumtp  15459  bpoly3  15766  strle3  16859  estrreslem2  17853  estrres  17854  lsptpcl  20239  perfectlem2  26376  ex-un  28784  ex-ss  28787  ex-pw  28789  ex-hash  28813  fnimatp  31010  prodtp  31137  sltsolem1  33874  dvh4dimlem  39453  dvhdimlem  39454  dvh4dimN  39457  tr3dom  41114  df3o2  41604  df3o3  41605  perfectALTVlem2  45143