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

Definition df-sym 26104
Description: The symbols of a grammar  g. Experimental. (Contributed by FL, 15-Jul-2012.)
Assertion
Ref Expression
df-sym  |-  sym  =  ( g  e.  Grammar  |->  ( ( ( 1st  o.  1st ) `  g )  u.  ( ( 2nd 
o.  1st ) `  g
) ) )

Detailed syntax breakdown of Definition df-sym
StepHypRef Expression
1 csym 26103 . 2  class  sym
2 vg . . 3  set  g
3 cgrm 26101 . . 3  class  Grammar
42cv 1631 . . . . 5  class  g
5 c1st 6136 . . . . . 6  class  1st
65, 5ccom 4709 . . . . 5  class  ( 1st 
o.  1st )
74, 6cfv 5271 . . . 4  class  ( ( 1st  o.  1st ) `  g )
8 c2nd 6137 . . . . . 6  class  2nd
98, 5ccom 4709 . . . . 5  class  ( 2nd 
o.  1st )
104, 9cfv 5271 . . . 4  class  ( ( 2nd  o.  1st ) `  g )
117, 10cun 3163 . . 3  class  ( ( ( 1st  o.  1st ) `  g )  u.  ( ( 2nd  o.  1st ) `  g ) )
122, 3, 11cmpt 4093 . 2  class  ( g  e.  Grammar  |->  ( ( ( 1st  o.  1st ) `  g )  u.  (
( 2nd  o.  1st ) `  g )
) )
131, 12wceq 1632 1  wff  sym  =  ( g  e.  Grammar  |->  ( ( ( 1st  o.  1st ) `  g )  u.  ( ( 2nd 
o.  1st ) `  g
) ) )
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator