Theorem or0 102

Description: Disjunction with 0. (Contributed by NM, 10-Aug-1997.)

Assertion

Ref	Expression
or0	(a ∪ 0) = a

Proof of Theorem or0

Step	Hyp	Ref	Expression
1		dff2 100	. . . 4 0 = (a ∪ a⊥ )⊥
2		ax-a2 31	. . . . 5 (a ∪ a⊥ ) = (a⊥ ∪ a)
3	2	ax-r4 37	. . . 4 (a ∪ a⊥ )⊥ = (a⊥ ∪ a)⊥
4	1, 3	ax-r2 36	. . 3 0 = (a⊥ ∪ a)⊥
5	4	lor 70	. 2 (a ∪ 0) = (a ∪ (a⊥ ∪ a)⊥ )
6		ax-a5 34	. 2 (a ∪ (a⊥ ∪ a)⊥ ) = a
7	5, 6	ax-r2 36	1 (a ∪ 0) = a

Syntax hints:   = wb 1  ^⊥ wn 4   ∪ wo 6  0wf 9

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

This theorem depends on definitions:  df-t 41  df-f 42

This theorem is referenced by:  or0r  103  an1  106  oridm  110  1b  117  le0  147  comm0  178  wwoml3  213  skr0  242  i3id  251  1i1  274  2vwomlem  365  wom5  381  wle0  390  oml3  452  oml4  487  gsth  489  i3bi  496  lem4  511  i3abs3  524  ud2lem1  563  ud3lem1a  566  ud3lem1b  567  ud3lem1  570  ud3lem2  571  ud3lem3d  575  ud3lem3  576  ud4lem1a  577  ud4lem1b  578  ud4lem1d  580  ud4lem2  582  ud4lem3  585  ud5lem1a  586  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  u1lemn1b  730  u2lem1  735  u4lem4  759  u2lem5  762  u4lem5  764  u4lem6  768  u2lem8  782  u3lem11  786  u3lem13a  789  u3lem13b  790  u3lem15  795  3vded21  817  3vded3  819  1oa  820  2oath1  826  bi3  839  bi4  840  mlaconj4  844  neg3antlem2  865  comanblem1  870  comanblem2  871  mhlem  876  mhlem1  877  marsdenlem3  882  marsdenlem4  883  mlaconjo  886  mhcor1  888  e2astlem1  895  govar  896  oa6v4v  933  oa3-2lema  978  oa3-1lem  982  oa3-6to3  987  oa3-2to4  988  oa3-2to2s  990  lem3.3.7i4e1  1069  lem3.3.7i5e1  1072