Definition df-tp 4635

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

Note: ordered triples are a completely different object defined below in df-ot 4639. 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 4634	. 2 class {𝐴, 𝐵, 𝐶}
5	1, 2	cpr 4632	. . 3 class {𝐴, 𝐵}
6	3	csn 4630	. . 3 class {𝐶}
7	5, 6	cun 3942	. 2 class ({𝐴, 𝐵} ∪ {𝐶})
8	4, 7	wceq 1533	1 wff {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})

This definition is referenced by:  eltpg  4691  raltpg  4704  rextpg  4705  disjtpsn  4721  disjtp2  4722  tpeq1  4748  tpeq2  4749  tpeq3  4750  tpcoma  4756  tpass  4758  qdass  4759  tpidm12  4761  diftpsn3  4807  tpprceq3  4809  tppreqb  4810  snsstp1  4821  snsstp2  4822  snsstp3  4823  sstp  4839  tpss  4840  tpssi  4841  ord3ex  5387  dmtpop  6224  funtpg  6609  funtp  6611  fntpg  6614  funcnvtp  6617  ftpg  7165  fvtp1  7207  fvtp1g  7210  tpex  7750  fr3nr  7775  tpfi  9349  fztp  13592  hashtplei  14481  hashtpg  14482  s3tpop  14896  sumtp  15731  bpoly3  16038  strle3  17132  estrreslem2  18132  estrres  18133  lsptpcl  20875  perfectlem2  27208  sltsolem1  27654  ex-un  30306  ex-ss  30309  ex-pw  30311  ex-hash  30335  fnimatp  32544  prodtp  32675  dvh4dimlem  41046  dvhdimlem  41047  dvh4dimN  41050  df3o2  42884  df3o3  42885  omcl3g  42905  onsucunitp  42944  oaun3  42953  tr3dom  43100  perfectALTVlem2  47199