Definition df-a 40

Description: Define conjunction. (Contributed by NM, 9-Aug-1997.)

Assertion

Ref	Expression
df-a	(a ∩ b) = (a⊥ ∪ b⊥ )⊥

Detailed syntax breakdown of Definition df-a

Step	Hyp	Ref	Expression
1		wva	. . 3 term  a
2		wvb	. . 3 term  b
3	1, 2	wa 7	. 2 term  (a ∩ b)
4	1	wn 4	. . . 4 term  a⊥
5	2	wn 4	. . . 4 term  b⊥
6	4, 5	wo 6	. . 3 term  (a⊥ ∪ b⊥ )
7	6	wn 4	. 2 term  (a⊥ ∪ b⊥ )⊥
8	3, 7	wb 1	1 wff  (a ∩ b) = (a⊥ ∪ b⊥ )⊥

This definition is referenced by:  ancom  74  anass  76  lan  77  oran  87  anor1  88  anor2  89  oran3  93  dfb  94  dfnb  95  an1  106  an0  108  anidm  111  orabs  120  anabs  121  di  126  wwfh1  216  wwfh2  217  wwfh3  218  wwfh4  219  ka4lem  229  ni31  250  ud1lem0c  277  ud4lem0c  280  ud5lem0c  281  wran  369  wcomlem  382  wcomdr  421  wfh1  423  wfh2  424  wfh3  425  wfh4  426  wcom2an  428  woml6  436  omla  447  comcom  453  comdr  466  df2c1  468  fh1  469  fh2  470  fh3  471  fh4  472  com2an  484  gsth2  490  i3ran  535  i3con  551  ud1lem1  560  ud3lem3  576  ud4lem1b  578  ud4lem1c  579  ud4lem1  581  ud5lem1b  587  ud5lem1  589  ud5lem3  594  u4lemona  628  u1lemonb  635  u1lemnaa  640  u5lemnaa  644  u4lemnab  653  u5lemnab  654  u1lemnona  665  u2lemnona  666  u3lemnona  667  u4lemnona  668  u5lemnona  669  u1lemnonb  675  u2lemnonb  676  u3lemnonb  677  u4lemnonb  678  u5lemnonb  679  u3lem1n  741  u4lem1n  742  u5lem1n  743  u4lem3n  755  u5lem3n  756  u3lem12  788  i1abs  801  test2  803  2oath1  826  elimconslem  867  elimcons  868  mlaconjo  886  oa6todual  952  oa8todual  971  oal1  1000