Definition df-tp 4613

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

Note: ordered triples are a completely different object defined below in df-ot 4617. 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 4612	. 2 class {𝐴, 𝐵, 𝐶}
5	1, 2	cpr 4610	. . 3 class {𝐴, 𝐵}
6	3	csn 4608	. . 3 class {𝐶}
7	5, 6	cun 3931	. 2 class ({𝐴, 𝐵} ∪ {𝐶})
8	4, 7	wceq 1539	1 wff {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})

This definition is referenced by:  eltpg  4668  raltpg  4680  rextpg  4681  disjtpsn  4697  disjtp2  4698  tpeq1  4724  tpeq2  4725  tpeq3  4726  tpcoma  4732  tpass  4734  qdass  4735  tpidm12  4737  diftpsn3  4784  tpprceq3  4786  tppreqb  4787  snsstp1  4798  snsstp2  4799  snsstp3  4800  sstp  4818  tpss  4819  tpssi  4820  ord3ex  5369  dmtpop  6220  funtpg  6602  funtp  6604  fntpg  6607  funcnvtp  6610  fnimatpd  6974  ftpg  7157  fvtp1  7198  fvtp1g  7201  tpex  7749  fr3nr  7775  tpfi  9348  fztp  13603  hashtplei  14506  hashtpg  14507  hash3tpexb  14516  s3tpop  14931  s3rn  14986  sumtp  15768  bpoly3  16077  strle3  17180  estrreslem2  18158  estrres  18159  lsptpcl  20950  perfectlem2  27229  sltsolem1  27675  ex-un  30390  ex-ss  30393  ex-pw  30395  ex-hash  30419  prodtp  32776  gsumtp  33007  dvh4dimlem  41386  dvhdimlem  41387  dvh4dimN  41390  df3o2  43271  df3o3  43272  omcl3g  43292  onsucunitp  43331  oaun3  43340  tr3dom  43486  perfectALTVlem2  47655  isgrtri  47856  usgrexmpl2edg  47934