Definition df-not 130

Description: Define the negation operator. (Contributed by Mario Carneiro, 8-Oct-2014.)

Assertion

Ref	Expression
df-not	|- T. |= [~ = \p:* [p:* ==> F.]]

Detailed syntax breakdown of Definition df-not

Step	Hyp	Ref	Expression
1		kt 8	. 2 term T.
2		tne 120	. . 3 term ~
3		hb 3	. . . 4 type *
4		vp	. . . 4 var p
5	3, 4	tv 1	. . . . 5 term p:*
6		tfal 118	. . . . 5 term F.
7		tim 121	. . . . 5 term ==>
8	5, 6, 7	kbr 9	. . . 4 term [p:* ==> F.]
9	3, 4, 8	kl 6	. . 3 term \p:* [p:* ==> F.]
10		ke 7	. . 3 term =
11	2, 9, 10	kbr 9	. 2 term [~ = \p:* [p:* ==> F.]]
12	1, 11	wffMMJ2 11	1 wff T. |= [~ = \p:* [p:* ==> F.]]

This definition is referenced by:  wnot  138  notval  145