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

Definition df-tp 3608
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 3602 . 2  class  { A ,  B ,  C }
51, 2cpr 3601 . . 3  class  { A ,  B }
63csn 3600 . . 3  class  { C }
75, 6cun 3111 . 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  3636  raltpg  3644  rextpg  3645  tpeq1  3675  tpeq2  3676  tpeq3  3677  tpcoma  3683  tpass  3685  qdass  3686  tpidm12  3688  snsstp1  3726  snsstp2  3727  snsstp3  3728  sstp  3738  tpss  3739  ord3ex  4158  tpex  4477  fr3nr  4529  dmtpop  5122  funtp  5227  fvtp1  5644  tpfi  7086  fztp  10793  hashtplei  11331  strlemor3  13185  strle3  13189  lsptpcl  15684  perfectlem2  20417  ex-un  20740  ex-ss  20743  ex-pw  20745  axsltsolem1  23676  bpoly3  24154  ftp  26246  dvh4dimlem  30784  dvhdimlem  30785  dvh4dimN  30788
  Copyright terms: Public domain W3C validator