Definition df-m0s

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

	Ref	Expression
Assertion	df-m0s	$$⊢\mathrm{m0St}=\left(a\in \mathrm{V}⟼⟨\varnothing ,\varnothing ,a⟩\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cm0s	$$class\mathrm{m0St}$$
1		va	$$setvara$$
2		cvv	$$class\mathrm{V}$$
3		c0	$$class\varnothing$$
4	1	cv	$$setvara$$
5	3 3 4	cotp	$$class⟨\varnothing ,\varnothing ,a⟩$$
6	1 2 5	cmpt	$$class\left(a\in \mathrm{V}⟼⟨\varnothing ,\varnothing ,a⟩\right)$$
7	0 6	wceq	$$wff\mathrm{m0St}=\left(a\in \mathrm{V}⟼⟨\varnothing ,\varnothing ,a⟩\right)$$