Definition df-eqfal 304

Description: A shorthand way of saying that a church-encoded value is false. Note that this is not the opposite of df-eqtru 303 (although they do exclude each other), since there are many more things an expression could equal.

Assertion

Ref	Expression
df-eqfal	⊦ (P = False ⧟ ⊭ P)

Detailed syntax breakdown of Definition df-eqfal

Step	Hyp	Ref	Expression
1		np	. . 3 nilad P
2		nfal 298	. . 3 nilad False
3	1, 2	weq 246	. 2 wff P = False
4	1	weqfal 302	. 2 wff ⊭ P
5	3, 4	wlb 55	1 wff (P = False ⧟ ⊭ P)

This definition is referenced by: (None)