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

Definition df-tp 3650
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 3644 . 2  class  { A ,  B ,  C }
51, 2cpr 3643 . . 3  class  { A ,  B }
63csn 3642 . . 3  class  { C }
75, 6cun 3152 . 2  class  ( { A ,  B }  u.  { C } )
84, 7wceq 1625 1  wff  { A ,  B ,  C }  =  ( { A ,  B }  u.  { C } )
Colors of variables: wff set class
This definition is referenced by:  eltpg  3678  raltpg  3686  rextpg  3687  tpeq1  3717  tpeq2  3718  tpeq3  3719  tpcoma  3725  tpass  3727  qdass  3728  tpidm12  3730  snsstp1  3768  snsstp2  3769  snsstp3  3770  sstp  3780  tpss  3781  ord3ex  4202  tpex  4521  fr3nr  4573  dmtpop  5151  funtp  5305  fvtp1  5726  tpfi  7134  fztp  10843  hashtplei  11382  strlemor3  13239  strle3  13243  lsptpcl  15738  perfectlem2  20471  ex-un  20813  ex-ss  20816  ex-pw  20818  sltsolem1  24324  bpoly3  24795  ftp  26904  diftpsneq  28081  tpprceq3  28083  dvh4dimlem  31706  dvhdimlem  31707  dvh4dimN  31710
  Copyright terms: Public domain W3C validator