Definition df-tp 4596

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

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

This definition is referenced by:  eltpg  4652  raltpg  4664  rextpg  4665  disjtpsn  4681  disjtp2  4682  tpeq1  4708  tpeq2  4709  tpeq3  4710  tpcoma  4716  tpass  4718  qdass  4719  tpidm12  4721  diftpsn3  4768  tpprceq3  4770  tppreqb  4771  snsstp1  4782  snsstp2  4783  snsstp3  4784  sstp  4802  tpss  4803  tpssi  4804  ord3ex  5344  dmtpop  6193  funtpg  6573  funtp  6575  fntpg  6578  funcnvtp  6581  fnimatpd  6947  ftpg  7130  fvtp1  7171  fvtp1g  7174  tpex  7724  fr3nr  7750  tpfi  9282  fztp  13547  hashtplei  14455  hashtpg  14456  hash3tpexb  14465  s3tpop  14881  s3rn  14936  sumtp  15721  bpoly3  16030  strle3  17136  estrreslem2  18105  estrres  18106  lsptpcl  20891  perfectlem2  27147  sltsolem1  27593  ex-un  30359  ex-ss  30362  ex-pw  30364  ex-hash  30388  tpssg  32472  prodtp  32758  gsumtp  33004  dvh4dimlem  41432  dvhdimlem  41433  dvh4dimN  41436  df3o2  43295  df3o3  43296  omcl3g  43316  onsucunitp  43355  oaun3  43364  tr3dom  43510  perfectALTVlem2  47713  isgrtri  47932  usgrexmpl2edg  48010