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

Definition df-tp 3501
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 3495 . 2  class  { A ,  B ,  C }
51, 2cpr 3494 . . 3  class  { A ,  B }
63csn 3493 . . 3  class  { C }
75, 6cun 3035 . 2  class  ( { A ,  B }  u.  { C } )
84, 7wceq 1314 1  wff  { A ,  B ,  C }  =  ( { A ,  B }  u.  { C } )
Colors of variables: wff set class
This definition is referenced by:  eltpg  3535  raltpg  3542  rextpg  3543  tpeq1  3575  tpeq2  3576  tpeq3  3577  tpcoma  3583  tpass  3585  qdass  3586  tpidm12  3588  diftpsn3  3627  snsstp1  3636  snsstp2  3637  snsstp3  3638  prsstp12  3639  tpss  3651  tpssi  3652  ord3ex  4074  tpexg  4325  dmtpop  4972  funtpg  5132  funtp  5134  fntpg  5137  ftpg  5558  fvtp1g  5582  tpfidisj  6769  fztp  9751  sumtp  11075  strle3g  11894  bdctp  12762
  Copyright terms: Public domain W3C validator