Theorem dff 93

Description: Alternate defintion of "false".

Assertion

Ref	Expression
dff	0 = (a ∩ a⊥ )

Proof of Theorem dff

Step	Hyp	Ref	Expression
1		dff2 92	. 2 0 = (a ∪ a⊥ )⊥
2		ancom 68	. . . 4 (a ∩ a⊥ ) = (a⊥ ∩ a)
3		anor2 81	. . . 4 (a⊥ ∩ a) = (a ∪ a⊥ )⊥
4	2, 3	ax-r2 35	. . 3 (a ∩ a⊥ ) = (a ∪ a⊥ )⊥
5	4	ax-r1 34	. 2 (a ∪ a⊥ )⊥ = (a ∩ a⊥ )
6	1, 5	ax-r2 35	1 0 = (a ∩ a⊥ )

Syntax hints:   = wb 1  ^⊥ wn 4   ∪ wo 6   ∩ wa 7  0wf 10

This theorem is referenced by:  wwfh1 208  wwfh2 209  ska8 228  i3id 243  go1 335  wfh1 405  wfh2 406  ortha 420  fh1 451  fh2 452  oml4 469  gsth 471  i3bi 478  lem4 493  i3abs3 506  ud2lem1 545  ud3lem1a 548  ud3lem1b 549  ud3lem1d 551  ud3lem2 553  ud3lem3b 555  ud3lem3d 557  ud4lem1a 559  ud4lem1b 560  ud4lem1d 562  ud4lem2 564  ud4lem3 567  ud5lem1a 568  ud5lem1b 569  ud5lem2 572  ud5lem3a 573  ud5lem3b 574  u1lemaa 582  u2lemaa 583  u3lemaa 584  u4lemaa 585  u5lemaa 586  u3lemana 589  u4lemana 590  u5lemana 591  u3lemab 594  u4lemab 595  u5lemab 596  u1lemanb 597  u2lemanb 598  u3lemanb 599  u4lemanb 600  u5lemanb 601  u3lemc4 685  u4lemc4 686  u1lemle2 697  u2lemle2 698  u4lemle2 700  u5lemle2 701  u5lembi 707  u2lem1 717  u4lem4 741  u4lem5 746  u4lem6 750  u2lem8 764  u3lem11 768  u3lem13a 771  u3lem13b 772  u3lem15 777  bi1o1a 780  3vded21 799  3vded3 801  1oa 802  mlalem 814  bi3 821  bi4 822  mlaconj4 826  neg3antlem2 847  comanblem1 852  comanblem2 853  mhlem1 859  mh 861  marsdenlem2 863  marsdenlem3 864  marsdenlem4 865  mlaconjo 868  mhcor1 870  govar 876  oa3-6to3 967  oa3-2to4 968

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-a 39  df-t 40  df-f 41

metamath.org