Definition df-id0 49

Description: Define classical identity.

Assertion

Ref	Expression
df-id0	(a ==0 b) = ((a' v b) ^ (b' v a))

Detailed syntax breakdown of Definition df-id0

Step	Hyp	Ref	Expression
1		wva	. . 3 term a
2		wvb	. . 3 term b
3	1, 2	wid0 17	. 2 term (a ==0 b)
4	1	wn 4	. . . 4 term a'
5	4, 2	wo 6	. . 3 term (a' v b)
6	2	wn 4	. . . 4 term b'
7	6, 1	wo 6	. . 3 term (b' v a)
8	5, 7	wa 7	. 2 term ((a' v b) ^ (b' v a))
9	3, 8	wb 1	1 wff (a ==0 b) = ((a' v b) ^ (b' v a))

This definition is referenced by:  nomcon0 301  nom20 313  nom30 319  nom50 331  nom60 337  id5leid0 351  lem3.3.7i0e1 1056  lem3.3.7i0e2 1057  wdid0id5 1108  wdid0id1 1109  wdid0id2 1110  wdid0id3 1111  wdid0id4 1112

Copyright terms: Public domain