Definition df-nse 243

Description: Definition of the dual write operator.

Assertion

Ref	Expression
df-nse	⊦ ([X ◁ Y] 𝜑 ⧟ ~ [X ≪ Y] ~ 𝜑)

Detailed syntax breakdown of Definition df-nse

Step	Hyp	Ref	Expression
1		wph	. . 3 wff 𝜑
2		nx	. . 3 nilad X
3		ny	. . 3 nilad Y
4	1, 2, 3	wnse 240	. 2 wff [X ◁ Y] 𝜑
5	1	wneg 3	. . . 4 wff ~ 𝜑
6	5, 2, 3	wse 204	. . 3 wff [X ≪ Y] ~ 𝜑
7	6	wneg 3	. 2 wff ~ [X ≪ Y] ~ 𝜑
8	4, 7	wlb 55	1 wff ([X ◁ Y] 𝜑 ⧟ ~ [X ≪ Y] ~ 𝜑)

This definition is referenced by: (None)