Definition df-id5 1046

Description: Define asymmetrical identity (for "Non-Orthomodular Models..." paper).

Assertion

Ref	Expression
df-id5	(a ==5 b) = ((a ^ b) v (a' ^ b'))

Detailed syntax breakdown of Definition df-id5

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

This definition is referenced by:  lem3.3.3lem1 1048  lem3.3.3lem2 1049  lem3.3.4 1052  lem3.3.7i5e1 1071  lem3.3.7i5e2 1072  lem3.4.3 1075  lem3.4.6 1078

Copyright terms: Public domain