Definition df-tp 4593

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

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

This definition is used by:  eltpg  4647  raltpg  4659  rextpg  4660  disjtpsn  4676  disjtp2  4677  tpeq1  4703  tpeq2  4704  tpeq3  4705  tpcoma  4711  tpass  4713  qdass  4714  tpidm12  4716  diftpsn3  4765  tpprceq3  4767  tppreqb  4768  snsstp1  4775  snsstp2  4776  snsstp3  4777  sstp  4794  tpss  4795  tpssi  4796  ord3ex  5353  dmtpop  6231  funtpg  6614  funtp  6616  fntpg  6619  funcnvtp  6622  fnimatpd  6989  xpsntpg  7165  ftpg  7181  fvtp1  7220  fvtp1g  7223  tpex  7783  fr3nr  7807  tpfi  9342  fztp  13738  hashtplei  14653  hashtpg  14654  hash3tpexb  14663  s3tpop  15086  s3rn  15143  sumtp  15941  bpoly3  16250  strle3  17364  estrreslem2  18338  estrres  18339  lsptpcl  21281  perfectlem2  27584  ltssolem1  28059  ex-un  31052  ex-ss  31055  ex-pw  31057  ex-hash  31081  tpssg  33202  prodtp  33485  gsumtp  33692  dvh4dimlem  42691  dvhdimlem  42692  dvh4dimN  42695  df3o2  44505  df3o3  44506  omcl3g  44526  onsucunitp  44565  oaun3  44574  tr3dom  44719  perfectALTVlem2  49023  isgrtri  49244  usgrexmpl2edg  49330