Definition df-tp 4637

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

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

This definition is referenced by:  eltpg  4692  raltpg  4704  rextpg  4705  disjtpsn  4721  disjtp2  4722  tpeq1  4748  tpeq2  4749  tpeq3  4750  tpcoma  4756  tpass  4758  qdass  4759  tpidm12  4761  diftpsn3  4808  tpprceq3  4810  tppreqb  4811  snsstp1  4822  snsstp2  4823  snsstp3  4824  sstp  4842  tpss  4843  tpssi  4844  ord3ex  5394  dmtpop  6243  funtpg  6626  funtp  6628  fntpg  6631  funcnvtp  6634  fnimatpd  6997  ftpg  7180  fvtp1  7219  fvtp1g  7222  tpex  7769  fr3nr  7795  tpfi  9369  fztp  13623  hashtplei  14526  hashtpg  14527  hash3tpexb  14536  s3tpop  14951  s3rn  15006  sumtp  15788  bpoly3  16097  strle3  17200  estrreslem2  18200  estrres  18201  lsptpcl  21001  perfectlem2  27297  sltsolem1  27743  ex-un  30466  ex-ss  30469  ex-pw  30471  ex-hash  30495  prodtp  32847  gsumtp  33057  dvh4dimlem  41438  dvhdimlem  41439  dvh4dimN  41442  df3o2  43317  df3o3  43318  omcl3g  43338  onsucunitp  43377  oaun3  43386  tr3dom  43532  perfectALTVlem2  47658  isgrtri  47859  usgrexmpl2edg  47937