Definition df-liff 317

Description: Church-encoding of logical biconditional.

Assertion

Ref	Expression
df-liff	⊦ Iff = λaλb(ba(Not' b))

Distinct variable group:   a,b

Detailed syntax breakdown of Definition df-liff

Step	Hyp	Ref	Expression
1		nliff 312	. 2 nilad Iff
2		va	. . 3 var a
3		vb	. . . 4 var b
4	3	nvar 203	. . . . 5 nilad b
5		nlnot 311	. . . . . 6 nilad Not
6	5, 4	nfv 281	. . . . 5 nilad (Not' b)
7	2	nvar 203	. . . . 5 nilad a
8	4, 6, 7	nov 284	. . . 4 nilad (ba(Not' b))
9	3, 8	nla 279	. . 3 nilad λb(ba(Not' b))
10	2, 9	nla 279	. 2 nilad λaλb(ba(Not' b))
11	1, 10	weq 246	1 wff Iff = λaλb(ba(Not' b))

This definition is referenced by: (None)