Definition df-tp 4324

Description: Define unordered triple of classes. Definition of [Enderton] p. 19. (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 4323	. 2 class {𝐴, 𝐵, 𝐶}
5	1, 2	cpr 4321	. . 3 class {𝐴, 𝐵}
6	3	csn 4319	. . 3 class {𝐶}
7	5, 6	cun 3711	. 2 class ({𝐴, 𝐵} ∪ {𝐶})
8	4, 7	wceq 1630	1 wff {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})

This definition is referenced by:  eltpg  4369  raltpg  4378  rextpg  4379  disjtpsn  4393  disjtp2  4394  tpeq1  4419  tpeq2  4420  tpeq3  4421  tpcoma  4427  tpass  4429  qdass  4430  tpidm12  4432  diftpsn3  4475  diftpsn3OLD  4476  tpprceq3  4478  tppreqb  4479  snsstp1  4490  snsstp2  4491  snsstp3  4492  sstp  4510  tpss  4511  tpssi  4512  ord3ex  5003  dmtpop  5768  funtpg  6101  funtpgOLD  6102  funtp  6104  fntpg  6107  funcnvtp  6110  ftpg  6584  fvtp1  6622  fvtp1g  6625  tpex  7120  fr3nr  7142  tpfi  8399  fztp  12588  hashtplei  13456  hashtpg  13457  s3tpop  13852  sumtp  14675  bpoly3  14986  strlemor3OLD  16171  strle3  16175  estrreslem2  16977  estrres  16978  lsptpcl  19179  perfectlem2  25152  ex-un  27590  ex-ss  27593  ex-pw  27595  ex-hash  27619  prodtp  29880  sltsolem1  32130  dvh4dimlem  37232  dvhdimlem  37233  dvh4dimN  37236  df3o2  38822  df3o3  38823  perfectALTVlem2  42139