Theorem dfb 94

Description: Biconditional expressed with others. (Contributed by NM, 10-Aug-1997.)

Assertion

Ref	Expression
dfb	(a ≡ b) = ((a ∩ b) ∪ (a⊥ ∩ b⊥ ))

Proof of Theorem dfb

Step	Hyp	Ref	Expression
1		df-b 39	. 2 (a ≡ b) = ((a⊥ ∪ b⊥ )⊥ ∪ (a ∪ b)⊥ )
2		df-a 40	. . . 4 (a ∩ b) = (a⊥ ∪ b⊥ )⊥
3	2	ax-r1 35	. . 3 (a⊥ ∪ b⊥ )⊥ = (a ∩ b)
4		oran 87	. . . 4 (a ∪ b) = (a⊥ ∩ b⊥ )⊥
5	4	con2 67	. . 3 (a ∪ b)⊥ = (a⊥ ∩ b⊥ )
6	3, 5	2or 72	. 2 ((a⊥ ∪ b⊥ )⊥ ∪ (a ∪ b)⊥ ) = ((a ∩ b) ∪ (a⊥ ∩ b⊥ ))
7	1, 6	ax-r2 36	1 (a ≡ b) = ((a ∩ b) ∪ (a⊥ ∩ b⊥ ))

Syntax hints:   = wb 1  ^⊥ wn 4   ≡ tb 5   ∪ wo 6   ∩ wa 7

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

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

This theorem is referenced by:  dfnb  95  bicom  96  lbi  97  biid  116  1b  117  conb  122  mi  125  wlem3.1  210  ka4lemo  228  ska13  241  wlem1  243  nom25  318  id5leid0  351  2vwomlem  365  wr2  371  wdf-c2  384  ska2  432  ska4  433  woml7  437  combi  485  oml4  487  i3bi  496  u1lembi  720  u2lembi  721  i2bi  722  u4lembi  724  u5lembi  725  u12lembi  726  u21lembi  727  bi1o1a  798  biao  799  mlalem  832  bi3  839  orbi  842  mlaconj4  844  comanblem2  871  mlaconjo  886  oa3-3lem  981  oa3-4lem  983  mloa  1018  wdcom  1105  wdid0id5  1111