Definition df-tp 4602

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

Note: ordered triples are a completely different object defined below in df-ot 4606. 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 4601	. 2 class {𝐴, 𝐵, 𝐶}
5	1, 2	cpr 4599	. . 3 class {𝐴, 𝐵}
6	3	csn 4597	. . 3 class {𝐶}
7	5, 6	cun 3920	. 2 class ({𝐴, 𝐵} ∪ {𝐶})
8	4, 7	wceq 1540	1 wff {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})

This definition is referenced by:  eltpg  4658  raltpg  4670  rextpg  4671  disjtpsn  4687  disjtp2  4688  tpeq1  4714  tpeq2  4715  tpeq3  4716  tpcoma  4722  tpass  4724  qdass  4725  tpidm12  4727  diftpsn3  4774  tpprceq3  4776  tppreqb  4777  snsstp1  4788  snsstp2  4789  snsstp3  4790  sstp  4808  tpss  4809  tpssi  4810  ord3ex  5350  dmtpop  6199  funtpg  6579  funtp  6581  fntpg  6584  funcnvtp  6587  fnimatpd  6952  ftpg  7135  fvtp1  7176  fvtp1g  7179  tpex  7729  fr3nr  7755  tpfi  9294  fztp  13554  hashtplei  14459  hashtpg  14460  hash3tpexb  14469  s3tpop  14885  s3rn  14940  sumtp  15722  bpoly3  16031  strle3  17136  estrreslem2  18105  estrres  18106  lsptpcl  20891  perfectlem2  27148  sltsolem1  27594  ex-un  30360  ex-ss  30363  ex-pw  30365  ex-hash  30389  tpssg  32473  prodtp  32760  gsumtp  33006  dvh4dimlem  41429  dvhdimlem  41430  dvh4dimN  41433  df3o2  43274  df3o3  43275  omcl3g  43295  onsucunitp  43334  oaun3  43343  tr3dom  43489  perfectALTVlem2  47678  isgrtri  47897  usgrexmpl2edg  47975