Definition df-fal

Description: Definition of the truth value "false", or "falsum", denoted by F. . See also df-tru . (Contributed by Anthony Hart, 22-Oct-2010)

	Ref	Expression
Assertion	df-fal	$$⊢\perp \leftrightarrow \neg \top$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		wfal	$$wff\perp$$
1		wtru	$$wff\top$$
2	1	wn	$$wff\neg \top$$
3	0 2	wb	$$wff\left(\perp \leftrightarrow \neg \top \right)$$