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 3947	. 2 class ({𝐴, 𝐵} ∪ {𝐶})
8	4, 7	wceq 1542	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  6218  funtpg  6604  funtp  6606  fntpg  6609  funcnvtp  6612  ftpg  7154  fvtp1  7196  fvtp1g  7199  tpex  7734  fr3nr  7759  tpfi  9323  fztp  13557  hashtplei  14445  hashtpg  14446  s3tpop  14860  sumtp  15695  bpoly3  16002  strle3  17093  estrreslem2  18090  estrres  18091  lsptpcl  20590  perfectlem2  26733  sltsolem1  27178  ex-un  29677  ex-ss  29680  ex-pw  29682  ex-hash  29706  fnimatp  31902  prodtp  32033  dvh4dimlem  40314  dvhdimlem  40315  dvh4dimN  40318  df3o2  42063  df3o3  42064  omcl3g  42084  onsucunitp  42123  oaun3  42132  tr3dom  42279  perfectALTVlem2  46390