df-fal - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > df-fal		Structured version Visualization version GIF version

Definition df-fal 1575

Description: Definition of the truth value "false", or "falsum", denoted by ⊥. See also df-tru 1565. (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 1574	. 2 wff ⊥
2		wtru 1563	. . 3 wff ⊤
3	2	wn 3	. 2 wff ¬ ⊤
4	1, 3	wb 208	1 wff (⊥ ↔ ¬ ⊤)

Colors of variables: wff setvar class

This definition is referenced by: fal 1576 nottru 1589 trunortru 1611 trunorfal 1612 empty 1928 bj-fal 37016 bj-cbvaew 37121 ralfal 45744