Definition df-tp 4653

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

Note: ordered triples are a completely different object defined below in df-ot 4657. 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 4652	. 2 class {𝐴, 𝐵, 𝐶}
5	1, 2	cpr 4650	. . 3 class {𝐴, 𝐵}
6	3	csn 4648	. . 3 class {𝐶}
7	5, 6	cun 3968	. 2 class ({𝐴, 𝐵} ∪ {𝐶})
8	4, 7	wceq 1537	1 wff {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})

This definition is referenced by:  eltpg  4709  raltpg  4723  rextpg  4724  disjtpsn  4740  disjtp2  4741  tpeq1  4767  tpeq2  4768  tpeq3  4769  tpcoma  4775  tpass  4777  qdass  4778  tpidm12  4780  diftpsn3  4827  tpprceq3  4829  tppreqb  4830  snsstp1  4841  snsstp2  4842  snsstp3  4843  sstp  4861  tpss  4862  tpssi  4863  ord3ex  5408  dmtpop  6248  funtpg  6632  funtp  6634  fntpg  6637  funcnvtp  6640  fnimatpd  7004  ftpg  7188  fvtp1  7230  fvtp1g  7233  tpex  7777  fr3nr  7803  tpfi  9389  fztp  13636  hashtplei  14529  hashtpg  14530  hash3tpexb  14539  s3tpop  14954  s3rn  15009  sumtp  15793  bpoly3  16100  strle3  17202  estrreslem2  18202  estrres  18203  lsptpcl  20995  perfectlem2  27283  sltsolem1  27729  ex-un  30447  ex-ss  30450  ex-pw  30452  ex-hash  30476  prodtp  32823  gsumtp  33031  dvh4dimlem  41348  dvhdimlem  41349  dvh4dimN  41352  df3o2  43215  df3o3  43216  omcl3g  43236  onsucunitp  43275  oaun3  43284  tr3dom  43430  perfectALTVlem2  47528  isgrtri  47723  usgrexmpl2edg  47763