Definition df-tp 4530

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

Note: ordered triples are a completely different object defined below in df-ot 4534. 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 4529	. 2 class {𝐴, 𝐵, 𝐶}
5	1, 2	cpr 4527	. . 3 class {𝐴, 𝐵}
6	3	csn 4525	. . 3 class {𝐶}
7	5, 6	cun 3879	. 2 class ({𝐴, 𝐵} ∪ {𝐶})
8	4, 7	wceq 1538	1 wff {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})

This definition is referenced by:  eltpg  4583  raltpg  4594  rextpg  4595  disjtpsn  4611  disjtp2  4612  tpeq1  4638  tpeq2  4639  tpeq3  4640  tpcoma  4646  tpass  4648  qdass  4649  tpidm12  4651  diftpsn3  4695  tpprceq3  4697  tppreqb  4698  snsstp1  4709  snsstp2  4710  snsstp3  4711  sstp  4727  tpss  4728  tpssi  4729  ord3ex  5253  dmtpop  6042  funtpg  6379  funtp  6381  fntpg  6384  funcnvtp  6387  ftpg  6895  fvtp1  6934  fvtp1g  6937  tpex  7450  fr3nr  7474  tpfi  8778  fztp  12958  hashtplei  13838  hashtpg  13839  s3tpop  14262  sumtp  15096  bpoly3  15404  strle3  16586  estrreslem2  17380  estrres  17381  lsptpcl  19744  perfectlem2  25814  ex-un  28209  ex-ss  28212  ex-pw  28214  ex-hash  28238  fnimatp  30440  prodtp  30569  sltsolem1  33293  dvh4dimlem  38739  dvhdimlem  38740  dvh4dimN  38743  tr3dom  40236  df3o2  40727  df3o3  40728  perfectALTVlem2  44240