Definition df-m0s 32837

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

Assertion

Ref	Expression
df-m0s	⊢ m0St = (𝑎 ∈ V ↦ ⟨∅, ∅, 𝑎⟩)

Detailed syntax breakdown of Definition df-m0s

Step	Hyp	Ref	Expression
1		cm0s 32827	. 2 class m0St
2		va	. . 3 setvar 𝑎
3		cvv 3494	. . 3 class V
4		c0 4290	. . . 4 class ∅
5	2	cv 1532	. . . 4 class 𝑎
6	4, 4, 5	cotp 4568	. . 3 class ⟨∅, ∅, 𝑎⟩
7	2, 3, 6	cmpt 5138	. 2 class (𝑎 ∈ V ↦ ⟨∅, ∅, 𝑎⟩)
8	1, 7	wceq 1533	1 wff m0St = (𝑎 ∈ V ↦ ⟨∅, ∅, 𝑎⟩)

This definition is referenced by: (None)