Definition df-id5 1047

Description: Define asymmetrical identity (for "Non-Orthomodular Models..." paper). (Contributed by Roy F. Longton, 27-Jun-2005.)

Assertion

Ref	Expression
df-id5	(a ≡5 b) = ((a ∩ b) ∪ (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) ∪ (a⊥ ∩ b⊥ ))
9	3, 8	wb 1	1 wff  (a ≡5 b) = ((a ∩ b) ∪ (a⊥ ∩ b⊥ ))

This definition is referenced by:  lem3.3.3lem1  1049  lem3.3.3lem2  1050  lem3.3.4  1053  lem3.3.7i5e1  1072  lem3.3.7i5e2  1073  lem3.4.3  1076  lem3.4.6  1079