Definition df-iota 293

Description: Definition of the iota combinator in terms of S and K.

Assertion

Ref	Expression
df-iota	⊦ ι = λf((f' S)' K)

Detailed syntax breakdown of Definition df-iota

Step	Hyp	Ref	Expression
1		niota 289	. 2 nilad ι
2		vf	. . 3 var f
3	2	nvar 203	. . . . 5 nilad f
4		nss 286	. . . . 5 nilad S
5	3, 4	nfv 281	. . . 4 nilad (f' S)
6		nkk 287	. . . 4 nilad K
7	5, 6	nfv 281	. . 3 nilad ((f' S)' K)
8	2, 7	nla 279	. 2 nilad λf((f' S)' K)
9	1, 8	weq 246	1 wff ι = λf((f' S)' K)

This definition is referenced by: (None)