Definition df-tp 4566

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

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

This definition is referenced by:  eltpg  4621  raltpg  4634  rextpg  4635  disjtpsn  4651  disjtp2  4652  tpeq1  4678  tpeq2  4679  tpeq3  4680  tpcoma  4686  tpass  4688  qdass  4689  tpidm12  4691  diftpsn3  4735  tpprceq3  4737  tppreqb  4738  snsstp1  4749  snsstp2  4750  snsstp3  4751  sstp  4767  tpss  4768  tpssi  4769  ord3ex  5310  dmtpop  6121  funtpg  6489  funtp  6491  fntpg  6494  funcnvtp  6497  ftpg  7028  fvtp1  7070  fvtp1g  7073  tpex  7597  fr3nr  7622  tpfi  9090  fztp  13312  hashtplei  14198  hashtpg  14199  s3tpop  14622  sumtp  15461  bpoly3  15768  strle3  16861  estrreslem2  17855  estrres  17856  lsptpcl  20241  perfectlem2  26378  ex-un  28788  ex-ss  28791  ex-pw  28793  ex-hash  28817  fnimatp  31014  prodtp  31141  sltsolem1  33878  dvh4dimlem  39457  dvhdimlem  39458  dvh4dimN  39461  tr3dom  41135  df3o2  41634  df3o3  41635  perfectALTVlem2  45174