Definition df-tp 4592

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

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

This definition is used by:  eltpg  4650  raltpg  4662  rextpg  4663  disjtpsn  4679  disjtp2  4680  tpeq1  4706  tpeq2  4707  tpeq3  4708  tpcoma  4714  tpass  4716  qdass  4717  tpidm12  4719  diftpsn3  4768  tpprceq3  4770  tppreqb  4771  snsstp1  4780  snsstp2  4781  snsstp3  4782  sstp  4799  tpss  4800  tpssi  4801  ord3ex  5356  dmtpop  6218  funtpg  6592  funtp  6594  fntpg  6597  funcnvtp  6600  fnimatpd  6966  xpsntpg  7140  ftpg  7156  fvtp1  7196  fvtp1g  7199  tpex  7750  fr3nr  7774  tpfi  9298  fztp  13637  hashtplei  14551  hashtpg  14552  hash3tpexb  14561  s3tpop  14982  s3rn  15039  sumtp  15837  bpoly3  16148  strle3  17256  estrreslem2  18230  estrres  18231  lsptpcl  21164  perfectlem2  27464  ltssolem1  27909  ex-un  30890  ex-ss  30893  ex-pw  30895  ex-hash  30919  tpssg  32998  prodtp  33284  gsumtp  33491  dvh4dimlem  42303  dvhdimlem  42304  dvh4dimN  42307  df3o2  44141  df3o3  44142  omcl3g  44162  onsucunitp  44201  oaun3  44210  tr3dom  44355  perfectALTVlem2  48625  isgrtri  48846  usgrexmpl2edg  48932