Definition df-tp 4182

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 4181	. 2 class {𝐴, 𝐵, 𝐶}
5	1, 2	cpr 4179	. . 3 class {𝐴, 𝐵}
6	3	csn 4177	. . 3 class {𝐶}
7	5, 6	cun 3572	. 2 class ({𝐴, 𝐵} ∪ {𝐶})
8	4, 7	wceq 1483	1 wff {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})

This definition is referenced by:  eltpg  4227  raltpg  4236  rextpg  4237  disjtpsn  4251  disjtp2  4252  tpeq1  4277  tpeq2  4278  tpeq3  4279  tpcoma  4285  tpass  4287  qdass  4288  tpidm12  4290  diftpsn3  4332  diftpsn3OLD  4333  tpprceq3  4335  tppreqb  4336  snsstp1  4347  snsstp2  4348  snsstp3  4349  sstp  4367  tpss  4368  tpssi  4369  ord3ex  4856  dmtpop  5611  funtpg  5942  funtpgOLD  5943  funtp  5945  fntpg  5948  funcnvtp  5951  ftpg  6423  fvtp1  6460  fvtp1g  6463  tpex  6957  fr3nr  6979  tpfi  8236  fztp  12397  hashtplei  13266  hashtpg  13267  s3tpop  13654  sumtp  14478  bpoly3  14789  strlemor3OLD  15971  strle3  15975  estrreslem2  16778  estrres  16779  lsptpcl  18979  perfectlem2  24955  ex-un  27281  ex-ss  27284  ex-pw  27286  ex-hash  27310  prodtp  29573  sltsolem1  31826  dvh4dimlem  36732  dvhdimlem  36733  dvh4dimN  36736  df3o2  38322  df3o3  38323  perfectALTVlem2  41631