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

Definition df-id0 49
Description: Define classical identity. (Contributed by NM, 7-Feb-1999.)
Assertion
Ref Expression
df-id0 (a0 b) = ((ab) ∩ (ba))

Detailed syntax breakdown of Definition df-id0
StepHypRef Expression
1 wva . . 3 term  a
2 wvb . . 3 term  b
31, 2wid0 17 . 2 term  (a0 b)
41wn 4 . . . 4 term  a
54, 2wo 6 . . 3 term  (ab)
62wn 4 . . . 4 term  b
76, 1wo 6 . . 3 term  (ba)
85, 7wa 7 . 2 term  ((ab) ∩ (ba))
93, 8wb 1 1 wff  (a0 b) = ((ab) ∩ (ba))
Colors of variables: term
This definition is referenced by:  nomcon0  301  nom20  313  nom30  319  nom50  331  nom60  337  id5leid0  351  lem3.3.7i0e1  1057  lem3.3.7i0e2  1058  wdid0id5  1111  wdid0id1  1112  wdid0id2  1113  wdid0id3  1114  wdid0id4  1115
  Copyright terms: Public domain W3C validator