Definition df-tp 4578

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

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

This definition is referenced by:  eltpg  4636  raltpg  4648  rextpg  4649  disjtpsn  4665  disjtp2  4666  tpeq1  4692  tpeq2  4693  tpeq3  4694  tpcoma  4700  tpass  4702  qdass  4703  tpidm12  4705  diftpsn3  4751  tpprceq3  4753  tppreqb  4754  snsstp1  4765  snsstp2  4766  snsstp3  4767  sstp  4785  tpss  4786  tpssi  4787  ord3ex  5323  dmtpop  6165  funtpg  6536  funtp  6538  fntpg  6541  funcnvtp  6544  fnimatpd  6906  ftpg  7089  fvtp1  7129  fvtp1g  7132  tpex  7679  fr3nr  7705  tpfi  9210  fztp  13480  hashtplei  14391  hashtpg  14392  hash3tpexb  14401  s3tpop  14816  s3rn  14871  sumtp  15656  bpoly3  15965  strle3  17071  estrreslem2  18044  estrres  18045  lsptpcl  20912  perfectlem2  27168  sltsolem1  27614  ex-un  30404  ex-ss  30407  ex-pw  30409  ex-hash  30433  tpssg  32517  prodtp  32810  gsumtp  33038  dvh4dimlem  41552  dvhdimlem  41553  dvh4dimN  41556  df3o2  43416  df3o3  43417  omcl3g  43437  onsucunitp  43476  oaun3  43485  tr3dom  43631  perfectALTVlem2  47832  isgrtri  48053  usgrexmpl2edg  48139