Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-m0s Structured version   Visualization version   Unicode version
Definition df-m0s 31492
Description: Define a function mapping expressions to statements. (Contributed by Mario Carneiro, 14-Jul-2016.)
Assertion
Ref Expression
df-m0s |- m0St = ( a e. _V |-> <. (/) , (/) , a >. )
Detailed syntax breakdown of Definition df-m0s
StepHypRef Expression
1 cm0s 31482 . 2 class m0St
2 va . . 3 setvar a
3 cvv 3200 . . 3 class _V
4 c0 3915 . . . 4 class (/)
52cv 1482 . . . 4 class a
64, 4, 5cotp 4185 . . 3 class <. (/) , (/) , a >.
72, 3, 6cmpt 4729 . 2 class ( a e. _V |-> <. (/) , (/) , a >. )
81, 7wceq 1483 1 wff m0St = ( a e. _V |-> <. (/) , (/) , a >. )
Colors of variables: wff setvar class
This definition is referenced by: (None)
  Copyright terms: Public domain W3C validator