Definition df-b1 1048

Description: Define biconditional for →₁ . (Contributed by Roy F. Longton, 27-Jun-2005.)

Assertion

Ref	Expression
df-b1	(a ↔1 b) = ((a →1 b) ∩ (b →1 a))

Detailed syntax breakdown of Definition df-b1

Step	Hyp	Ref	Expression
1		wva	. . 3 term  a
2		wvb	. . 3 term  b
3	1, 2	wb1 24	. 2 term  (a ↔1 b)
4	1, 2	wi1 12	. . 3 term  (a →1 b)
5	2, 1	wi1 12	. . 3 term  (b →1 a)
6	4, 5	wa 7	. 2 term  ((a →1 b) ∩ (b →1 a))
7	3, 6	wb 1	1 wff  (a ↔1 b) = ((a →1 b) ∩ (b →1 a))

This definition is referenced by:  lem3.3.3  1052  lem3.3.5  1055