Definition df-tp 4573

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

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

This definition is referenced by:  eltpg  4631  raltpg  4643  rextpg  4644  disjtpsn  4660  disjtp2  4661  tpeq1  4687  tpeq2  4688  tpeq3  4689  tpcoma  4695  tpass  4697  qdass  4698  tpidm12  4700  diftpsn3  4748  tpprceq3  4750  tppreqb  4751  snsstp1  4760  snsstp2  4761  snsstp3  4762  sstp  4780  tpss  4781  tpssi  4782  ord3ex  5328  dmtpop  6180  funtpg  6551  funtp  6553  fntpg  6556  funcnvtp  6559  fnimatpd  6922  ftpg  7107  fvtp1  7147  fvtp1g  7150  tpex  7697  fr3nr  7723  tpfi  9233  fztp  13531  hashtplei  14443  hashtpg  14444  hash3tpexb  14453  s3tpop  14868  s3rn  14923  sumtp  15708  bpoly3  16020  strle3  17127  estrreslem2  18101  estrres  18102  lsptpcl  20971  perfectlem2  27190  ltssolem1  27636  ex-un  30491  ex-ss  30494  ex-pw  30496  ex-hash  30520  tpssg  32604  prodtp  32897  gsumtp  33122  dvh4dimlem  41886  dvhdimlem  41887  dvh4dimN  41890  df3o2  43738  df3o3  43739  omcl3g  43759  onsucunitp  43798  oaun3  43807  tr3dom  43952  perfectALTVlem2  48189  isgrtri  48410  usgrexmpl2edg  48496