Definition df-fal 1561

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

Assertion

Ref	Expression
df-fal	⊢ (⊥ ↔ ¬ ⊤)

Detailed syntax breakdown of Definition df-fal

Step	Hyp	Ref	Expression
1		wfal 1560	. 2 wff ⊥
2		wtru 1549	. . 3 wff ⊤
3	2	wn 3	. 2 wff ¬ ⊤
4	1, 3	wb 208	1 wff (⊥ ↔ ¬ ⊤)

This definition is referenced by:  fal  1562  nottru  1575  trunortru  1597  trunorfal  1598  empty  1914  bj-fal  36892  bj-cbvaew  36997  ralfal  45620