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

Definition df-tp 3648
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 3642 . 2  class  { A ,  B ,  C }
51, 2cpr 3641 . . 3  class  { A ,  B }
63csn 3640 . . 3  class  { C }
75, 6cun 3150 . 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  3676  raltpg  3684  rextpg  3685  tpeq1  3715  tpeq2  3716  tpeq3  3717  tpcoma  3723  tpass  3725  qdass  3726  tpidm12  3728  snsstp1  3766  snsstp2  3767  snsstp3  3768  sstp  3778  tpss  3779  ord3ex  4200  tpex  4519  fr3nr  4571  dmtpop  5149  funtp  5303  fvtp1  5724  tpfi  7132  fztp  10841  hashtplei  11380  strlemor3  13237  strle3  13241  lsptpcl  15736  perfectlem2  20469  ex-un  20811  ex-ss  20814  ex-pw  20816  sltsolem1  24322  bpoly3  24793  ftp  26893  diftpsneq  28070  tpprceq3  28072  dvh4dimlem  31633  dvhdimlem  31634  dvh4dimN  31637
  Copyright terms: Public domain W3C validator