Definition df-b 38

Description: Define biconditional.

Assertion

Ref	Expression
df-b	(a == b) = ((a_|_ v b_|_)_|_ v (a v 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_|_ v b_|_)
7	6	wn 4	. . 3 term (a_|_ v b_|_)_|_
8	1, 2	wo 6	. . . 4 term (a v b)
9	8	wn 4	. . 3 term (a v b)_|_
10	7, 9	wo 6	. 2 term ((a_|_ v b_|_)_|_ v (a v b)_|_)
11	3, 10	wb 1	1 wff (a == b) = ((a_|_ v b_|_)_|_ v (a v b)_|_)

This definition is referenced by:  dfb 86  wa6 188  r3a 422

metamath.org