Definition df-id0 49

Description: Define classical identity. (Contributed by NM, 7-Feb-1999.)

Assertion

Ref	Expression
df-id0	(a ≡0 b) = ((a⊥ ∪ b) ∩ (b⊥ ∪ a))

Detailed syntax breakdown of Definition df-id0

Step	Hyp	Ref	Expression
1		wva	. . 3 term  a
2		wvb	. . 3 term  b
3	1, 2	wid0 17	. 2 term  (a ≡0 b)
4	1	wn 4	. . . 4 term  a⊥
5	4, 2	wo 6	. . 3 term  (a⊥ ∪ b)
6	2	wn 4	. . . 4 term  b⊥
7	6, 1	wo 6	. . 3 term  (b⊥ ∪ a)
8	5, 7	wa 7	. 2 term  ((a⊥ ∪ b) ∩ (b⊥ ∪ a))
9	3, 8	wb 1	1 wff  (a ≡0 b) = ((a⊥ ∪ b) ∩ (b⊥ ∪ a))

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