Definition df-tp 4563

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

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

This definition is referenced by:  eltpg  4618  raltpg  4631  rextpg  4632  disjtpsn  4648  disjtp2  4649  tpeq1  4675  tpeq2  4676  tpeq3  4677  tpcoma  4683  tpass  4685  qdass  4686  tpidm12  4688  diftpsn3  4732  tpprceq3  4734  tppreqb  4735  snsstp1  4746  snsstp2  4747  snsstp3  4748  sstp  4764  tpss  4765  tpssi  4766  ord3ex  5304  dmtpop  6109  funtpg  6470  funtp  6472  fntpg  6475  funcnvtp  6478  ftpg  7007  fvtp1  7049  fvtp1g  7052  tpex  7572  fr3nr  7597  tpfi  8995  fztp  13216  hashtplei  14101  hashtpg  14102  s3tpop  14525  sumtp  15364  bpoly3  15671  strle3  16764  estrreslem2  17746  estrres  17747  lsptpcl  20131  perfectlem2  26258  ex-un  28664  ex-ss  28667  ex-pw  28669  ex-hash  28693  fnimatp  30891  prodtp  31018  sltsolem1  33780  dvh4dimlem  39363  dvhdimlem  39364  dvh4dimN  39367  tr3dom  41005  df3o2  41496  df3o3  41497  perfectALTVlem2  45035