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

Definition df-tp 3623
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 3617 . 2  class  { A ,  B ,  C }
51, 2cpr 3616 . . 3  class  { A ,  B }
63csn 3615 . . 3  class  { C }
75, 6cun 3125 . 2  class  ( { A ,  B }  u.  { C } )
84, 7wceq 1619 1  wff  { A ,  B ,  C }  =  ( { A ,  B }  u.  { C } )
Colors of variables: wff set class
This definition is referenced by:  eltpg  3651  raltpg  3659  rextpg  3660  tpeq1  3690  tpeq2  3691  tpeq3  3692  tpcoma  3698  tpass  3700  qdass  3701  tpidm12  3703  snsstp1  3741  snsstp2  3742  snsstp3  3743  sstp  3753  tpss  3754  ord3ex  4173  tpex  4492  fr3nr  4544  dmtpop  5121  funtp  5242  fvtp1  5659  tpfi  7101  fztp  10809  hashtplei  11347  strlemor3  13201  strle3  13205  lsptpcl  15700  perfectlem2  20433  ex-un  20756  ex-ss  20759  ex-pw  20761  axsltsolem1  23692  bpoly3  24170  ftp  26262  dvh4dimlem  30892  dvhdimlem  30893  dvh4dimN  30896
  Copyright terms: Public domain W3C validator