MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-tp Structured version   Unicode version

Definition df-tp 3939
Description: Define unordered triple of classes. Definition of [Enderton] p. 19. (Contributed by NM, 9-Apr-1994.)
Assertion
Ref Expression
df-tp  |-  { A ,  B ,  C }  =  ( { A ,  B }  u.  { C } )

Detailed syntax breakdown of Definition df-tp
StepHypRef Expression
1 cA . . 3  class  A
2 cB . . 3  class  B
3 cC . . 3  class  C
41, 2, 3ctp 3938 . 2  class  { A ,  B ,  C }
51, 2cpr 3936 . . 3  class  { A ,  B }
63csn 3934 . . 3  class  { C }
75, 6cun 3370 . 2  class  ( { A ,  B }  u.  { C } )
84, 7wceq 1437 1  wff  { A ,  B ,  C }  =  ( { A ,  B }  u.  { C } )
Colors of variables: wff setvar class
This definition is referenced by:  eltpg  3978  raltpg  3987  rextpg  3988  tpeq1  4024  tpeq2  4025  tpeq3  4026  tpcoma  4032  tpass  4034  qdass  4035  tpidm12  4037  diftpsn3  4074  tpprceq3  4076  tppreqb  4077  snsstp1  4087  snsstp2  4088  snsstp3  4089  sstp  4100  tpss  4101  tpssi  4102  ord3ex  4550  dmtpop  5267  funtpg  5587  funtp  5589  fntpg  5592  ftpg  6026  fvtp1  6063  fvtp1g  6066  tpex  6541  fr3nr  6557  tpfi  7793  fztp  11796  hashtplei  12581  hashtpg  12582  sumtp  13746  bpoly3  14047  strlemor3  15155  strle3  15159  estrreslem2  15959  estrres  15960  lsptpcl  18138  perfectlem2  24093  constr2spthlem1  25259  ex-un  25809  ex-ss  25812  ex-pw  25814  sltsolem1  30499  dvh4dimlem  34917  dvhdimlem  34918  dvh4dimN  34921  perfectALTVlem2  38651
  Copyright terms: Public domain W3C validator