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

Definition df-tp 3438
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 3432 . 2  class  { A ,  B ,  C }
51, 2cpr 3431 . . 3  class  { A ,  B }
63csn 3430 . . 3  class  { C }
75, 6cun 2986 . 2  class  ( { A ,  B }  u.  { C } )
84, 7wceq 1287 1  wff  { A ,  B ,  C }  =  ( { A ,  B }  u.  { C } )
Colors of variables: wff set class
This definition is referenced by:  eltpg  3470  raltpg  3477  rextpg  3478  tpeq1  3510  tpeq2  3511  tpeq3  3512  tpcoma  3518  tpass  3520  qdass  3521  tpidm12  3523  diftpsn3  3560  snsstp1  3569  snsstp2  3570  snsstp3  3571  prsstp12  3572  tpss  3584  tpssi  3585  ord3ex  3997  tpexg  4241  dmtpop  4868  funtpg  5026  funtp  5028  fntpg  5031  ftpg  5437  fvtp1g  5459  fztp  9414  bdctp  11192
  Copyright terms: Public domain W3C validator