QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  df-id1 GIF version

Definition df-id1 50
Description: Define asymmetrical identity (for "Non-Orthomodular Models..." paper). (Contributed by NM, 7-Feb-1999.)
Assertion
Ref Expression
df-id1 (a1 b) = ((ab ) ∩ (a ∪ (ab)))

Detailed syntax breakdown of Definition df-id1
StepHypRef Expression
1 wva . . 3 term  a
2 wvb . . 3 term  b
31, 2wid1 18 . 2 term  (a1 b)
42wn 4 . . . 4 term  b
51, 4wo 6 . . 3 term  (ab )
61wn 4 . . . 4 term  a
71, 2wa 7 . . . 4 term  (ab)
86, 7wo 6 . . 3 term  (a ∪ (ab))
95, 8wa 7 . 2 term  ((ab ) ∩ (a ∪ (ab)))
103, 9wb 1 1 wff  (a1 b) = ((ab ) ∩ (a ∪ (ab)))
Colors of variables: term
This definition is referenced by:  nomb41  299  nomcon1  302  nomcon2  303  nom21  314  nom52  333  lem3.3.7i1e1  1060  lem3.3.7i1e2  1061  thm3.8i1lem  1080  wdid0id1  1112
  Copyright terms: Public domain W3C validator