Definition df-b 39

Description: Define biconditional. (Contributed by NM, 9-Aug-1997.)

Assertion

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

Detailed syntax breakdown of Definition df-b

Step	Hyp	Ref	Expression
1		wva	. . 3 term  a
2		wvb	. . 3 term  b
3	1, 2	tb 5	. 2 term  (a ≡ b)
4	1	wn 4	. . . . 5 term  a⊥
5	2	wn 4	. . . . 5 term  b⊥
6	4, 5	wo 6	. . . 4 term  (a⊥ ∪ b⊥ )
7	6	wn 4	. . 3 term  (a⊥ ∪ b⊥ )⊥
8	1, 2	wo 6	. . . 4 term  (a ∪ b)
9	8	wn 4	. . 3 term  (a ∪ b)⊥
10	7, 9	wo 6	. 2 term  ((a⊥ ∪ b⊥ )⊥ ∪ (a ∪ b)⊥ )
11	3, 10	wb 1	1 wff  (a ≡ b) = ((a⊥ ∪ b⊥ )⊥ ∪ (a ∪ b)⊥ )

This definition is used by:  dfb  94  wa6  196  r3a  440