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

Definition df-tp 3414
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 3408 . 2  class  { A ,  B ,  C }
51, 2cpr 3407 . . 3  class  { A ,  B }
63csn 3406 . . 3  class  { C }
75, 6cun 2972 . 2  class  ( { A ,  B }  u.  { C } )
84, 7wceq 1285 1  wff  { A ,  B ,  C }  =  ( { A ,  B }  u.  { C } )
Colors of variables: wff set class
This definition is referenced by:  eltpg  3446  raltpg  3453  rextpg  3454  tpeq1  3486  tpeq2  3487  tpeq3  3488  tpcoma  3494  tpass  3496  qdass  3497  tpidm12  3499  diftpsn3  3535  snsstp1  3543  snsstp2  3544  snsstp3  3545  prsstp12  3546  tpss  3558  tpssi  3559  ord3ex  3969  tpexg  4205  dmtpop  4826  funtpg  4981  funtp  4983  fntpg  4986  ftpg  5379  fvtp1g  5401  fztp  9171  bdctp  10821
  Copyright terms: Public domain W3C validator