Definition df-lnot 316

Description: Church-encoding of logical negation.

Assertion

Ref	Expression
df-lnot	⊦ Not = λaλxλy(yax)

Distinct variable group:   a,x,y

Detailed syntax breakdown of Definition df-lnot

Step	Hyp	Ref	Expression
1		nlnot 311	. 2 nilad Not
2		va	. . 3 var a
3		vx	. . . 4 var x
4		vy	. . . . 5 var y
5	4	nvar 203	. . . . . 6 nilad y
6	3	nvar 203	. . . . . 6 nilad x
7	2	nvar 203	. . . . . 6 nilad a
8	5, 6, 7	nov 284	. . . . 5 nilad (yax)
9	4, 8	nla 279	. . . 4 nilad λy(yax)
10	3, 9	nla 279	. . 3 nilad λxλy(yax)
11	2, 10	nla 279	. 2 nilad λaλxλy(yax)
12	1, 11	weq 246	1 wff Not = λaλxλy(yax)

This definition is referenced by: (None)