Definition df-tp 4586

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

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

This definition is referenced by:  eltpg  4644  raltpg  4656  rextpg  4657  disjtpsn  4673  disjtp2  4674  tpeq1  4700  tpeq2  4701  tpeq3  4702  tpcoma  4708  tpass  4710  qdass  4711  tpidm12  4713  diftpsn3  4759  tpprceq3  4761  tppreqb  4762  snsstp1  4773  snsstp2  4774  snsstp3  4775  sstp  4793  tpss  4794  tpssi  4795  ord3ex  5333  dmtpop  6177  funtpg  6548  funtp  6550  fntpg  6553  funcnvtp  6556  fnimatpd  6919  ftpg  7103  fvtp1  7143  fvtp1g  7146  tpex  7693  fr3nr  7719  tpfi  9230  fztp  13500  hashtplei  14411  hashtpg  14412  hash3tpexb  14421  s3tpop  14836  s3rn  14891  sumtp  15676  bpoly3  15985  strle3  17091  estrreslem2  18065  estrres  18066  lsptpcl  20934  perfectlem2  27201  ltssolem1  27647  ex-un  30503  ex-ss  30506  ex-pw  30508  ex-hash  30532  tpssg  32615  prodtp  32910  gsumtp  33149  dvh4dimlem  41771  dvhdimlem  41772  dvh4dimN  41775  df3o2  43622  df3o3  43623  omcl3g  43643  onsucunitp  43682  oaun3  43691  tr3dom  43836  perfectALTVlem2  48035  isgrtri  48256  usgrexmpl2edg  48342