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

Definition df-tp 3589
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 3583 . 2  class  { A ,  B ,  C }
51, 2cpr 3582 . . 3  class  { A ,  B }
63csn 3581 . . 3  class  { C }
75, 6cun 3092 . 2  class  ( { A ,  B }  u.  { C } )
84, 7wceq 1619 1  wff  { A ,  B ,  C }  =  ( { A ,  B }  u.  { C } )
Colors of variables: wff set class
This definition is referenced by:  eltpg  3617  raltpg  3625  rextpg  3626  tpeq1  3656  tpeq2  3657  tpeq3  3658  tpcoma  3664  tpass  3666  qdass  3667  tpidm12  3669  snsstp1  3707  snsstp2  3708  snsstp3  3709  sstp  3719  tpss  3720  ord3ex  4138  tpex  4456  fr3nr  4508  dmtpop  5101  funtp  5206  fvtp1  5623  tpfi  7065  fztp  10772  hashtplei  11310  strlemor3  13164  strle3  13168  lsptpcl  15663  perfectlem2  20396  ex-un  20719  ex-ss  20722  ex-pw  20724  axsltsolem1  23655  bpoly3  24133  ftp  26225  dvh4dimlem  30763  dvhdimlem  30764  dvh4dimN  30767
  Copyright terms: Public domain W3C validator