Definition df-a 39

Description: Define conjunction.

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 68  anass 69  lan 70  oran 79  anor1 80  anor2 81  oran3 85  dfb 86  dfnb 87  an1 98  an0 100  anidm 103  a5b 112  a5c 113  di 118  wwfh1 208  wwfh2 209  wwfh3 210  wwfh4 211  ka4lem 221  ni31 242  ud1lem0c 269  ud4lem0c 272  ud5lem0c 273  wran 351  wcomlem 364  wcomdr 403  wfh1 405  wfh2 406  wfh3 407  wfh4 408  wcom2an 410  woml6 418  omla 429  comcom 435  comdr 448  df2c1 450  fh1 451  fh2 452  fh3 453  fh4 454  com2an 466  gsth2 472  i3ran 517  i3con 533  ud1lem1 542  ud3lem3 558  ud4lem1b 560  ud4lem1c 561  ud4lem1 563  ud5lem1b 569  ud5lem1 571  ud5lem3 576  u4lemona 610  u1lemonb 617  u1lemnaa 622  u5lemnaa 626  u4lemnab 635  u5lemnab 636  u1lemnona 647  u2lemnona 648  u3lemnona 649  u4lemnona 650  u5lemnona 651  u1lemnonb 657  u2lemnonb 658  u3lemnonb 659  u4lemnonb 660  u5lemnonb 661  u3lem1n 723  u4lem1n 724  u5lem1n 725  u4lem3n 737  u5lem3n 738  u3lem12 770  i1abs 783  test2 785  2oath1 808  elimconslem 849  elimcons 850  mlaconjo 868  oa6todual 932  oa8todual 951  oal1 980

metamath.org