Definition df-not 130

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

Assertion

Ref	Expression
df-not	⊢ ⊤⊧[¬ = λp:∗ [p:∗ ⇒ ⊥]]

Detailed syntax breakdown of Definition df-not

Step	Hyp	Ref	Expression
1		kt 8	. 2 term ⊤
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 ⊥
7		tim 121	. . . . 5 term ⇒
8	5, 6, 7	kbr 9	. . . 4 term [p:∗ ⇒ ⊥]
9	3, 4, 8	kl 6	. . 3 term λp:∗ [p:∗ ⇒ ⊥]
10		ke 7	. . 3 term =
11	2, 9, 10	kbr 9	. 2 term [¬ = λp:∗ [p:∗ ⇒ ⊥]]
12	1, 11	wffMMJ2 11	1 wff ⊤⊧[¬ = λp:∗ [p:∗ ⇒ ⊥]]

This definition is referenced by:  wnot  138  notval  145