Definition df-id1 49

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

Assertion

Ref	Expression
df-id1	(a ==1 b) = ((a v b_|_) ^ (a_|_ v (a ^ b)))

Detailed syntax breakdown of Definition df-id1

Step	Hyp	Ref	Expression
1		wva	. . 3 term a
2		wvb	. . 3 term b
3	1, 2	wid1 19	. 2 term (a ==1 b)
4	2	wn 4	. . . 4 term b_|_
5	1, 4	wo 6	. . 3 term (a v b_|_)
6	1	wn 4	. . . 4 term a_|_
7	1, 2	wa 7	. . . 4 term (a ^ b)
8	6, 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 ==1 b) = ((a v b_|_) ^ (a_|_ v (a ^ b)))

This definition is referenced by:  nomb41 291  nomcon1 294  nomcon2 295  nom21 306  nom52 325

metamath.org