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

Definition df-tp 3782
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 3776 . 2  class  { A ,  B ,  C }
51, 2cpr 3775 . . 3  class  { A ,  B }
63csn 3774 . . 3  class  { C }
75, 6cun 3278 . 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  3811  raltpg  3819  rextpg  3820  tpeq1  3852  tpeq2  3853  tpeq3  3854  tpcoma  3860  tpass  3862  qdass  3863  tpidm12  3865  diftpsn3  3897  tpprceq3  3898  tppreqb  3899  snsstp1  3909  snsstp2  3910  snsstp3  3911  sstp  3923  tpss  3924  tpssi  3925  ord3ex  4349  tpex  4667  fr3nr  4719  dmtpop  5305  funtpg  5460  funtp  5462  fntpg  5465  ftpg  5875  fvtp1  5898  fvtp1g  5901  tpfi  7341  fztp  11058  hashtplei  11645  hashtpg  11646  strlemor3  13513  strle3  13517  lsptpcl  16010  perfectlem2  20967  constr2spthlem1  21547  ex-un  21685  ex-ss  21688  ex-pw  21690  sltsolem1  25536  bpoly3  26008  dvh4dimlem  31926  dvhdimlem  31927  dvh4dimN  31930
  Copyright terms: Public domain W3C validator