Definition df-id2 51

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

Assertion

Ref	Expression
df-id2	(a ==2 b) = ((a v b') ^ (b v (a' ^ b')))

Detailed syntax breakdown of Definition df-id2

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

This definition is referenced by:  nomb32 300  nomcon1 302  nomcon2 303  nom22 315  nom51 332  lem3.3.7i2e1 1062  lem3.3.7i2e2 1063  wdid0id2 1110

Copyright terms: Public domain