Definition df-m0s 33557

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 33547	. 2 class m0St
2		va	. . 3 setvar 𝑎
3		cvv 3432	. . 3 class V
4		c0 4256	. . . 4 class ∅
5	2	cv 1538	. . . 4 class 𝑎
6	4, 4, 5	cotp 4569	. . 3 class ⟨∅, ∅, 𝑎⟩
7	2, 3, 6	cmpt 5157	. 2 class (𝑎 ∈ V ↦ ⟨∅, ∅, 𝑎⟩)
8	1, 7	wceq 1539	1 wff m0St = (𝑎 ∈ V ↦ ⟨∅, ∅, 𝑎⟩)

This definition is referenced by: (None)