Definition df-id3 51

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

Assertion

Ref	Expression
df-id3	(a ==3 b) = ((a_|_ v b) ^ (a v (a_|_ ^ b_|_)))

Detailed syntax breakdown of Definition df-id3

Step	Hyp	Ref	Expression
1		wva	. . 3 term a
2		wvb	. . 3 term b
3	1, 2	wid3 21	. 2 term (a ==3 b)
4	1	wn 4	. . . 4 term a_|_
5	4, 2	wo 6	. . 3 term (a_|_ v b)
6	2	wn 4	. . . . 5 term b_|_
7	4, 6	wa 7	. . . 4 term (a_|_ ^ b_|_)
8	1, 7	wo 6	. . 3 term (a v (a_|_ ^ b_|_))
9	5, 8	wa 7	. 2 term ((a_|_ v b) ^ (a v (a_|_ ^ b_|_)))
10	3, 9	wb 1	1 wff (a ==3 b) = ((a_|_ v b) ^ (a v (a_|_ ^ b_|_)))

This definition is referenced by:  nomb32 292  nom23 308  nom54 327

metamath.org