Definition df-tp 4572

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 4571	. 2 class {𝐴, 𝐵, 𝐶}
5	1, 2	cpr 4569	. . 3 class {𝐴, 𝐵}
6	3	csn 4567	. . 3 class {𝐶}
7	5, 6	cun 3934	. 2 class ({𝐴, 𝐵} ∪ {𝐶})
8	4, 7	wceq 1537	1 wff {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})

This definition is referenced by:  eltpg  4623  raltpg  4634  rextpg  4635  disjtpsn  4651  disjtp2  4652  tpeq1  4678  tpeq2  4679  tpeq3  4680  tpcoma  4686  tpass  4688  qdass  4689  tpidm12  4691  diftpsn3  4735  tpprceq3  4737  tppreqb  4738  snsstp1  4749  snsstp2  4750  snsstp3  4751  sstp  4767  tpss  4768  tpssi  4769  ord3ex  5288  dmtpop  6075  funtpg  6409  funtp  6411  fntpg  6414  funcnvtp  6417  ftpg  6918  fvtp1  6957  fvtp1g  6960  tpex  7470  fr3nr  7494  tpfi  8794  fztp  12964  hashtplei  13843  hashtpg  13844  s3tpop  14271  sumtp  15104  bpoly3  15412  strle3  16594  estrreslem2  17388  estrres  17389  lsptpcl  19751  perfectlem2  25806  ex-un  28203  ex-ss  28206  ex-pw  28208  ex-hash  28232  fnimatp  30423  prodtp  30543  sltsolem1  33180  dvh4dimlem  38594  dvhdimlem  38595  dvh4dimN  38598  tr3dom  39914  df3o2  40394  df3o3  40395  perfectALTVlem2  43907