Theorem or0 102

Description: Disjunction with 0.

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 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 1068  lem3.3.7i5e1 1071

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

Copyright terms: Public domain