Definition df-id0 48

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 18	. 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 293  nom20 305  nom30 311  nom50 323  nom60 329

metamath.org