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

Definition df-tp 3505
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 3499 . 2  class  { A ,  B ,  C }
51, 2cpr 3498 . . 3  class  { A ,  B }
63csn 3497 . . 3  class  { C }
75, 6cun 3039 . 2  class  ( { A ,  B }  u.  { C } )
84, 7wceq 1316 1  wff  { A ,  B ,  C }  =  ( { A ,  B }  u.  { C } )
Colors of variables: wff set class
This definition is referenced by:  eltpg  3539  raltpg  3546  rextpg  3547  tpeq1  3579  tpeq2  3580  tpeq3  3581  tpcoma  3587  tpass  3589  qdass  3590  tpidm12  3592  diftpsn3  3631  snsstp1  3640  snsstp2  3641  snsstp3  3642  prsstp12  3643  tpss  3655  tpssi  3656  ord3ex  4084  tpexg  4335  dmtpop  4984  funtpg  5144  funtp  5146  fntpg  5149  ftpg  5572  fvtp1g  5596  tpfidisj  6784  fztp  9813  sumtp  11138  strle3g  11962  bdctp  12966
  Copyright terms: Public domain W3C validator