Users' Mathboxes Mathbox for Frédéric Liné < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-psc Unicode version

Definition df-psc 26129
Description: Definition of the symbol  ps. Experimental. (Contributed by FL, 2-Feb-2014.)
Assertion
Ref Expression
df-psc  |-  ps c  =  { <. 1 ,  8
>. }

Detailed syntax breakdown of Definition df-psc
StepHypRef Expression
1 clpsc 26128 . 2  class  ps c
2 c1 8754 . . . 4  class  1
3 c8 9817 . . . 4  class  8
42, 3cop 3656 . . 3  class  <. 1 ,  8 >.
54csn 3653 . 2  class  { <. 1 ,  8 >. }
61, 5wceq 1632 1  wff  ps c  =  { <. 1 ,  8
>. }
Colors of variables: wff set class
This definition is referenced by:  psckle  26131  pspf  26154  pgapspf  26155
  Copyright terms: Public domain W3C validator