Definition df-tp 4634

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

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

This definition is referenced by:  eltpg  4690  raltpg  4703  rextpg  4704  disjtpsn  4720  disjtp2  4721  tpeq1  4747  tpeq2  4748  tpeq3  4749  tpcoma  4755  tpass  4757  qdass  4758  tpidm12  4760  diftpsn3  4806  tpprceq3  4808  tppreqb  4809  snsstp1  4820  snsstp2  4821  snsstp3  4822  sstp  4838  tpss  4839  tpssi  4840  ord3ex  5386  dmtpop  6222  funtpg  6607  funtp  6609  fntpg  6612  funcnvtp  6615  ftpg  7163  fvtp1  7205  fvtp1g  7208  tpex  7748  fr3nr  7773  tpfi  9347  fztp  13589  hashtplei  14477  hashtpg  14478  s3tpop  14892  sumtp  15727  bpoly3  16034  strle3  17128  estrreslem2  18128  estrres  18129  lsptpcl  20867  perfectlem2  27193  sltsolem1  27638  ex-un  30290  ex-ss  30293  ex-pw  30295  ex-hash  30319  fnimatp  32520  prodtp  32647  dvh4dimlem  40985  dvhdimlem  40986  dvh4dimN  40989  df3o2  42807  df3o3  42808  omcl3g  42828  onsucunitp  42867  oaun3  42876  tr3dom  43023  perfectALTVlem2  47125