Definition df-kk 291

Description: Definition of the K combinator.

Assertion

Ref	Expression
df-kk	⊦ K = λaλba

Distinct variable group:   a,b

Detailed syntax breakdown of Definition df-kk

Step	Hyp	Ref	Expression
1		nkk 287	. 2 nilad K
2		va	. . 3 var a
3		vb	. . . 4 var b
4	2	nvar 203	. . . 4 nilad a
5	3, 4	nla 279	. . 3 nilad λba
6	2, 5	nla 279	. 2 nilad λaλba
7	1, 6	weq 246	1 wff K = λaλba

This definition is referenced by: (None)