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

Definition df-tp 3649
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 3643 . 2  class  { A ,  B ,  C }
51, 2cpr 3642 . . 3  class  { A ,  B }
63csn 3641 . . 3  class  { C }
75, 6cun 3151 . 2  class  ( { A ,  B }  u.  { C } )
84, 7wceq 1623 1  wff  { A ,  B ,  C }  =  ( { A ,  B }  u.  { C } )
Colors of variables: wff set class
This definition is referenced by:  eltpg  3677  raltpg  3685  rextpg  3686  tpeq1  3716  tpeq2  3717  tpeq3  3718  tpcoma  3724  tpass  3726  qdass  3727  tpidm12  3729  snsstp1  3767  snsstp2  3768  snsstp3  3769  sstp  3779  tpss  3780  ord3ex  4199  tpex  4518  fr3nr  4570  dmtpop  5147  funtp  5269  fvtp1  5686  tpfi  7128  fztp  10837  hashtplei  11376  strlemor3  13233  strle3  13237  lsptpcl  15732  perfectlem2  20465  ex-un  20788  ex-ss  20791  ex-pw  20793  axsltsolem1  23725  bpoly3  24203  ftp  26304  dvh4dimlem  30912  dvhdimlem  30913  dvh4dimN  30916
  Copyright terms: Public domain W3C validator