Definition df-id1 50

Description: Define asymmetrical identity (for "Non-Orthomodular Models..." paper). (Contributed by NM, 7-Feb-1999.)

Assertion

Ref	Expression
df-id1	(a ≡1 b) = ((a ∪ b⊥ ) ∩ (a⊥ ∪ (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 18	. 2 term  (a ≡1 b)
4	2	wn 4	. . . 4 term  b⊥
5	1, 4	wo 6	. . 3 term  (a ∪ 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⊥ ∪ (a ∩ b))
9	5, 8	wa 7	. 2 term  ((a ∪ b⊥ ) ∩ (a⊥ ∪ (a ∩ b)))
10	3, 9	wb 1	1 wff  (a ≡1 b) = ((a ∪ b⊥ ) ∩ (a⊥ ∪ (a ∩ b)))

This definition is used by:  nomb41  299  nomcon1  302  nomcon2  303  nom21  314  nom52  333  lem3.3.7i1e1  1060  lem3.3.7i1e2  1061  thm3.8i1lem  1080  wdid0id1  1112