Definition df-tp 4582

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

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

This definition is referenced by:  eltpg  4638  raltpg  4650  rextpg  4651  disjtpsn  4667  disjtp2  4668  tpeq1  4694  tpeq2  4695  tpeq3  4696  tpcoma  4702  tpass  4704  qdass  4705  tpidm12  4707  diftpsn3  4753  tpprceq3  4755  tppreqb  4756  snsstp1  4767  snsstp2  4768  snsstp3  4769  sstp  4787  tpss  4788  tpssi  4789  ord3ex  5326  dmtpop  6167  funtpg  6537  funtp  6539  fntpg  6542  funcnvtp  6545  fnimatpd  6907  ftpg  7090  fvtp1  7131  fvtp1g  7134  tpex  7682  fr3nr  7708  tpfi  9215  fztp  13483  hashtplei  14391  hashtpg  14392  hash3tpexb  14401  s3tpop  14816  s3rn  14871  sumtp  15656  bpoly3  15965  strle3  17071  estrreslem2  18044  estrres  18045  lsptpcl  20882  perfectlem2  27139  sltsolem1  27585  ex-un  30368  ex-ss  30371  ex-pw  30373  ex-hash  30397  tpssg  32481  prodtp  32773  gsumtp  33012  dvh4dimlem  41432  dvhdimlem  41433  dvh4dimN  41436  df3o2  43296  df3o3  43297  omcl3g  43317  onsucunitp  43356  oaun3  43365  tr3dom  43511  perfectALTVlem2  47716  isgrtri  47937  usgrexmpl2edg  48023