Definition df-tp 4590

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

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

This definition is referenced by:  eltpg  4646  raltpg  4658  rextpg  4659  disjtpsn  4675  disjtp2  4676  tpeq1  4702  tpeq2  4703  tpeq3  4704  tpcoma  4710  tpass  4712  qdass  4713  tpidm12  4715  diftpsn3  4762  tpprceq3  4764  tppreqb  4765  snsstp1  4776  snsstp2  4777  snsstp3  4778  sstp  4796  tpss  4797  tpssi  4798  ord3ex  5337  dmtpop  6179  funtpg  6555  funtp  6557  fntpg  6560  funcnvtp  6563  fnimatpd  6927  ftpg  7110  fvtp1  7151  fvtp1g  7154  tpex  7702  fr3nr  7728  tpfi  9252  fztp  13517  hashtplei  14425  hashtpg  14426  hash3tpexb  14435  s3tpop  14851  s3rn  14906  sumtp  15691  bpoly3  16000  strle3  17106  estrreslem2  18079  estrres  18080  lsptpcl  20917  perfectlem2  27174  sltsolem1  27620  ex-un  30403  ex-ss  30406  ex-pw  30408  ex-hash  30432  tpssg  32516  prodtp  32802  gsumtp  33041  dvh4dimlem  41430  dvhdimlem  41431  dvh4dimN  41434  df3o2  43295  df3o3  43296  omcl3g  43316  onsucunitp  43355  oaun3  43364  tr3dom  43510  perfectALTVlem2  47716  isgrtri  47935  usgrexmpl2edg  48013