Definition df-m0s

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cm0s	⊢ m0St
1		va	⊢ 𝑎
2		cvv	⊢ V
3		c0	⊢ ∅
4	1	cv	⊢ 𝑎
5	3 3 4	cotp	⊢ ⟨ ∅ , ∅ , 𝑎 ⟩
6	1 2 5	cmpt	⊢ ( 𝑎 ∈ V ↦ ⟨ ∅ , ∅ , 𝑎 ⟩ )
7	0 6	wceq	⊢ m0St = ( 𝑎 ∈ V ↦ ⟨ ∅ , ∅ , 𝑎 ⟩ )