Theorem dfb 86

Description: Biconditional expressed with others.

Assertion

Ref	Expression
dfb	(a == b) = ((a ^ b) v (a_|_ ^ b_|_))

Proof of Theorem dfb

Step	Hyp	Ref	Expression
1		df-b 38	. 2 (a == b) = ((a_|_ v b_|_)_|_ v (a v b)_|_)
2		df-a 39	. . . 4 (a ^ b) = (a_|_ v b_|_)_|_
3	2	ax-r1 34	. . 3 (a_|_ v b_|_)_|_ = (a ^ b)
4		oran 79	. . . 4 (a v b) = (a_|_ ^ b_|_)_|_
5	4	con2 64	. . 3 (a v b)_|_ = (a_|_ ^ b_|_)
6	3, 5	2or 67	. 2 ((a_|_ v b_|_)_|_ v (a v b)_|_) = ((a ^ b) v (a_|_ ^ b_|_))
7	1, 6	ax-r2 35	1 (a == b) = ((a ^ b) v (a_|_ ^ b_|_))

Syntax hints:   = wb 1  _|_wn 4   == tb 5   v wo 6   ^ wa 7

This theorem is referenced by:  dfnb 87  bicom 88  lbi 89  biid 108  1b 109  conb 114  mi 117  wlem3.1 202  ka4lemo 220  ska13 233  wlem1 235  nom25 310  2vwomlem 347  wr2 353  wdf-c2 366  ska2 414  ska4 415  woml7 419  lem3.1 425  combi 467  oml4 469  i3bi 478  u1lembi 702  u2lembi 703  i2bi 704  u4lembi 706  u5lembi 707  u12lembi 708  u21lembi 709  bi1o1a 780  biao 781  mlalem 814  bi3 821  orbi 824  mlaconj4 826  comanblem2 853  mlaconjo 868  oa3-3lem 961  oa3-4lem 963  mloa 998

This theorem was proved from axioms:  ax-a1 29  ax-a2 30  ax-r1 34  ax-r2 35  ax-r4 36  ax-r5 37

This theorem depends on definitions:  df-b 38  df-a 39

metamath.org