Definition df-m0s

Description: Define a function mapping expressions to statements. (Contributed by Mario Carneiro, 14-Jul-2016)

	Ref	Expression
Assertion	df-m0s	|- m0St = ( a e. _V |-> <. (/) , (/) , a >. )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cm0s	|- m0St
1		va	|- a
2		cvv	|- _V
3		c0	|- (/)
4	1	cv	|- a
5	3 3 4	cotp	|- <. (/) , (/) , a >.
6	1 2 5	cmpt	|- ( a e. _V |-> <. (/) , (/) , a >. )
7	0 6	wceq	|- m0St = ( a e. _V |-> <. (/) , (/) , a >. )