ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-tp Unicode version

Definition df-tp 3612
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 3606 . 2  class  { A ,  B ,  C }
51, 2cpr 3605 . . 3  class  { A ,  B }
63csn 3604 . . 3  class  { C }
75, 6cun 3139 . 2  class  ( { A ,  B }  u.  { C } )
84, 7wceq 1363 1  wff  { A ,  B ,  C }  =  ( { A ,  B }  u.  { C } )
Colors of variables: wff set class
This definition is referenced by:  eltpg  3649  raltpg  3657  rextpg  3658  tpeq1  3690  tpeq2  3691  tpeq3  3692  tpcoma  3698  tpass  3700  qdass  3701  tpidm12  3703  diftpsn3  3745  snsstp1  3754  snsstp2  3755  snsstp3  3756  prsstp12  3757  tpss  3770  tpssi  3771  ord3ex  4202  tpexg  4456  dmtpop  5116  funtpg  5279  funtp  5281  fntpg  5284  ftpg  5713  fvtp1g  5737  tpfidisj  6941  fztp  10092  sumtp  11436  strle3g  12582  lsptpcl  13583  bdctp  14920
  Copyright terms: Public domain W3C validator