Definition df-tp 4629

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

Note: ordered triples are a completely different object defined below in df-ot 4633. 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 4628	. 2 class {𝐴, 𝐵, 𝐶}
5	1, 2	cpr 4626	. . 3 class {𝐴, 𝐵}
6	3	csn 4624	. . 3 class {𝐶}
7	5, 6	cun 3942	. 2 class ({𝐴, 𝐵} ∪ {𝐶})
8	4, 7	wceq 1534	1 wff {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})

This definition is referenced by:  eltpg  4685  raltpg  4698  rextpg  4699  disjtpsn  4715  disjtp2  4716  tpeq1  4742  tpeq2  4743  tpeq3  4744  tpcoma  4750  tpass  4752  qdass  4753  tpidm12  4755  diftpsn3  4801  tpprceq3  4803  tppreqb  4804  snsstp1  4815  snsstp2  4816  snsstp3  4817  sstp  4833  tpss  4834  tpssi  4835  ord3ex  5381  dmtpop  6216  funtpg  6602  funtp  6604  fntpg  6607  funcnvtp  6610  ftpg  7159  fvtp1  7201  fvtp1g  7204  tpex  7743  fr3nr  7768  tpfi  9339  fztp  13581  hashtplei  14469  hashtpg  14470  s3tpop  14884  sumtp  15719  bpoly3  16026  strle3  17120  estrreslem2  18120  estrres  18121  lsptpcl  20852  perfectlem2  27150  sltsolem1  27595  ex-un  30221  ex-ss  30224  ex-pw  30226  ex-hash  30250  fnimatp  32446  prodtp  32572  dvh4dimlem  40853  dvhdimlem  40854  dvh4dimN  40857  df3o2  42665  df3o3  42666  omcl3g  42686  onsucunitp  42725  oaun3  42734  tr3dom  42881  perfectALTVlem2  46985