Definition df-tp 4562

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

Note: ordered triples are a completely different object defined below in df-ot 4566. 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 4561	. 2 class {𝐴, 𝐵, 𝐶}
5	1, 2	cpr 4559	. . 3 class {𝐴, 𝐵}
6	3	csn 4557	. . 3 class {𝐶}
7	5, 6	cun 3882	. 2 class ({𝐴, 𝐵} ∪ {𝐶})
8	4, 7	wceq 1548	1 wff {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})

This definition is referenced by:  eltpg  4620  raltpg  4632  rextpg  4633  disjtpsn  4649  disjtp2  4650  tpeq1  4676  tpeq2  4677  tpeq3  4678  tpcoma  4684  tpass  4686  qdass  4687  tpidm12  4689  diftpsn3  4737  tpprceq3  4739  tppreqb  4740  snsstp1  4749  snsstp2  4750  snsstp3  4751  sstp  4769  tpss  4770  tpssi  4771  ord3ex  5318  dmtpop  6172  funtpg  6543  funtp  6545  fntpg  6548  funcnvtp  6551  fnimatpd  6914  ftpg  7102  fvtp1  7142  fvtp1g  7145  tpex  7692  fr3nr  7718  tpfi  9230  fztp  13529  hashtplei  14441  hashtpg  14442  hash3tpexb  14451  s3tpop  14866  s3rn  14921  sumtp  15706  bpoly3  16018  strle3  17125  estrreslem2  18099  estrres  18100  lsptpcl  20972  perfectlem2  27214  ltssolem1  27659  ex-un  30514  ex-ss  30517  ex-pw  30519  ex-hash  30543  tpssg  32627  prodtp  32921  gsumtp  33147  dvh4dimlem  41948  dvhdimlem  41949  dvh4dimN  41952  df3o2  43771  df3o3  43772  omcl3g  43792  onsucunitp  43831  oaun3  43840  tr3dom  43985  perfectALTVlem2  48225  isgrtri  48446  usgrexmpl2edg  48532