Definition df-false-D2.5 158

Description: Definition of False, '⊥'.

Assertion

Ref	Expression
df-false-D2.5	⊢ (⊥ ↔ ¬ ⊤)

Detailed syntax breakdown of Definition df-false-D2.5

Step	Hyp	Ref	Expression
1		wff-false 157	. 2 wff ⊥
2		wff-true 153	. . 3 wff ⊤
3	2	wff-neg 9	. 2 wff ¬ ⊤
4	1, 3	wff-bi 104	1 wff (⊥ ↔ ¬ ⊤)

This definition is referenced by:  false-P2.15  159