Definition df-m0s 35563

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 35553	. 2 class m0St
2		va	. . 3 setvar 𝑎
3		cvv 3459	. . 3 class V
4		c0 4308	. . . 4 class ∅
5	2	cv 1539	. . . 4 class 𝑎
6	4, 4, 5	cotp 4609	. . 3 class ⟨∅, ∅, 𝑎⟩
7	2, 3, 6	cmpt 5201	. 2 class (𝑎 ∈ V ↦ ⟨∅, ∅, 𝑎⟩)
8	1, 7	wceq 1540	1 wff m0St = (𝑎 ∈ V ↦ ⟨∅, ∅, 𝑎⟩)

This definition is referenced by: (None)