Definition df-tp 4583

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

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

This definition is referenced by:  eltpg  4641  raltpg  4653  rextpg  4654  disjtpsn  4670  disjtp2  4671  tpeq1  4697  tpeq2  4698  tpeq3  4699  tpcoma  4705  tpass  4707  qdass  4708  tpidm12  4710  diftpsn3  4756  tpprceq3  4758  tppreqb  4759  snsstp1  4770  snsstp2  4771  snsstp3  4772  sstp  4790  tpss  4791  tpssi  4792  ord3ex  5330  dmtpop  6174  funtpg  6545  funtp  6547  fntpg  6550  funcnvtp  6553  fnimatpd  6916  ftpg  7099  fvtp1  7139  fvtp1g  7142  tpex  7689  fr3nr  7715  tpfi  9224  fztp  13494  hashtplei  14405  hashtpg  14406  hash3tpexb  14415  s3tpop  14830  s3rn  14885  sumtp  15670  bpoly3  15979  strle3  17085  estrreslem2  18059  estrres  18060  lsptpcl  20928  perfectlem2  27195  sltsolem1  27641  ex-un  30448  ex-ss  30451  ex-pw  30453  ex-hash  30477  tpssg  32561  prodtp  32857  gsumtp  33096  dvh4dimlem  41642  dvhdimlem  41643  dvh4dimN  41646  df3o2  43497  df3o3  43498  omcl3g  43518  onsucunitp  43557  oaun3  43566  tr3dom  43711  perfectALTVlem2  47910  isgrtri  48131  usgrexmpl2edg  48217