Theorem dff 101

Description: Alternate definition of "false". (Contributed by NM, 29-Aug-1997.)

Assertion

Ref	Expression
dff	0 = (a ∩ a⊥ )

Proof of Theorem dff

Step	Hyp	Ref	Expression
1		dff2 100	. 2 0 = (a ∪ a⊥ )⊥
2		ancom 74	. . . 4 (a ∩ a⊥ ) = (a⊥ ∩ a)
3		anor2 89	. . . 4 (a⊥ ∩ a) = (a ∪ a⊥ )⊥
4	2, 3	ax-r2 36	. . 3 (a ∩ a⊥ ) = (a ∪ a⊥ )⊥
5	4	ax-r1 35	. 2 (a ∪ a⊥ )⊥ = (a ∩ a⊥ )
6	1, 5	ax-r2 36	1 0 = (a ∩ a⊥ )

This proof depends on syntax axioms:   = wb 1  ^⊥ wn 4   ∪ wo 6   ∩ wa 7  0wf 9

This proof depends on axioms:  ax-a1 30  ax-a2 31  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38

This proof depends on definitions:  df-a 40  df-t 41  df-f 42

This theorem is used by:  wwfh1  216  wwfh2  217  ska8  236  i3id  251  go1  343  k1-4  359  wfh1  423  wfh2  424  ortha  438  fh1  469  fh2  470  oml4  487  gsth  489  i3bi  496  lem4  511  i3abs3  524  ud2lem1  563  ud3lem1a  566  ud3lem1b  567  ud3lem1d  569  ud3lem2  571  ud3lem3b  573  ud3lem3d  575  ud4lem1a  577  ud4lem1b  578  ud4lem1d  580  ud4lem2  582  ud4lem3  585  ud5lem1a  586  ud5lem1b  587  ud5lem2  590  ud5lem3a  591  ud5lem3b  592  u1lemaa  600  u2lemaa  601  u3lemaa  602  u4lemaa  603  u5lemaa  604  u3lemana  607  u4lemana  608  u5lemana  609  u3lemab  612  u4lemab  613  u5lemab  614  u1lemanb  615  u2lemanb  616  u3lemanb  617  u4lemanb  618  u5lemanb  619  u3lemc4  703  u4lemc4  704  u1lemle2  715  u2lemle2  716  u4lemle2  718  u5lemle2  719  u5lembi  725  u2lem1  735  u4lem4  759  u4lem5  764  u4lem6  768  u2lem8  782  u3lem11  786  u3lem13a  789  u3lem13b  790  u3lem15  795  bi1o1a  798  3vded21  817  3vded3  819  1oa  820  mlalem  832  bi3  839  bi4  840  mlaconj4  844  neg3antlem2  865  comanblem1  870  comanblem2  871  mhlem1  877  mh  879  marsdenlem2  881  marsdenlem3  882  marsdenlem4  883  mlaconjo  886  mhcor1  888  govar  896  oa3-6to3  987  oa3-2to4  988  lem3.3.7i3e1  1066