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

Definition df-tp 3786
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 3780 . 2  class  { A ,  B ,  C }
51, 2cpr 3779 . . 3  class  { A ,  B }
63csn 3778 . . 3  class  { C }
75, 6cun 3282 . 2  class  ( { A ,  B }  u.  { C } )
84, 7wceq 1649 1  wff  { A ,  B ,  C }  =  ( { A ,  B }  u.  { C } )
Colors of variables: wff set class
This definition is referenced by:  eltpg  3815  raltpg  3823  rextpg  3824  tpeq1  3856  tpeq2  3857  tpeq3  3858  tpcoma  3864  tpass  3866  qdass  3867  tpidm12  3869  diftpsn3  3901  tpprceq3  3902  tppreqb  3903  snsstp1  3913  snsstp2  3914  snsstp3  3915  sstp  3927  tpss  3928  tpssi  3929  ord3ex  4353  tpex  4671  fr3nr  4723  dmtpop  5309  funtpg  5464  funtp  5466  fntpg  5469  ftpg  5879  fvtp1  5902  fvtp1g  5905  tpfi  7345  fztp  11062  hashtplei  11649  hashtpg  11650  strlemor3  13517  strle3  13521  lsptpcl  16014  perfectlem2  20971  constr2spthlem1  21551  ex-un  21689  ex-ss  21692  ex-pw  21694  sltsolem1  25540  bpoly3  26012  dvh4dimlem  31930  dvhdimlem  31931  dvh4dimN  31934
  Copyright terms: Public domain W3C validator