Definition df-tp 4160

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 4159	. 2 class {𝐴, 𝐵, 𝐶}
5	1, 2	cpr 4157	. . 3 class {𝐴, 𝐵}
6	3	csn 4155	. . 3 class {𝐶}
7	5, 6	cun 3558	. 2 class ({𝐴, 𝐵} ∪ {𝐶})
8	4, 7	wceq 1480	1 wff {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})

This definition is referenced by:  eltpg  4205  raltpg  4214  rextpg  4215  disjtpsn  4228  disjtp2  4229  tpeq1  4254  tpeq2  4255  tpeq3  4256  tpcoma  4262  tpass  4264  qdass  4265  tpidm12  4267  diftpsn3  4308  diftpsn3OLD  4309  tpprceq3  4311  tppreqb  4312  snsstp1  4322  snsstp2  4323  snsstp3  4324  sstp  4342  tpss  4343  tpssi  4344  ord3ex  4826  dmtpop  5580  funtpg  5910  funtpgOLD  5911  funtp  5913  fntpg  5916  funcnvtp  5919  ftpg  6388  fvtp1  6425  fvtp1g  6428  tpex  6922  fr3nr  6941  tpfi  8196  fztp  12355  hashtplei  13220  hashtpg  13221  s3tpop  13606  sumtp  14427  bpoly3  14733  strlemor3OLD  15911  strle3  15915  estrreslem2  16718  estrres  16719  lsptpcl  18919  perfectlem2  24889  ex-un  27169  ex-ss  27172  ex-pw  27174  ex-hash  27198  sltsolem1  31581  dvh4dimlem  36251  dvhdimlem  36252  dvh4dimN  36255  df3o2  37843  df3o3  37844  perfectALTVlem2  40956