df-b - Quantum Logic Explorer

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

Definition df-b 39

Description: Define biconditional.

**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)^⊥ )

Colors of variables: term

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

Copyright terms: Public domain