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	⊢ ( ⊥ ↔ ¬ ⊤ )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		wfal	⊢ ⊥
1		wtru	⊢ ⊤
2	1	wn	⊢ ¬ ⊤
3	0 2	wb	⊢ ( ⊥ ↔ ¬ ⊤ )