Theorem or0r 103

Description: Disjunction with 0. (Contributed by NM, 26-Nov-1997.)

Assertion

Ref	Expression
or0r	(0 ∪ a) = a

Proof of Theorem or0r

Step	Hyp	Ref	Expression
1		ax-a2 31	. 2 (0 ∪ a) = (a ∪ 0)
2		or0 102	. 2 (a ∪ 0) = a
3	1, 2	ax-r2 36	1 (0 ∪ a) = a

Syntax hints:   = wb 1   ∪ 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:  k1-4  359  ud3lem1a  566  ud3lem1d  569  ud5lem1b  587  bi1o1a  798  bi3  839  bi4  840  mlaconj4  844  mhlemlem1  874  mhlem1  877  marsdenlem2  881  mlaconjo  886  mhcor1  888  e2astlem1  895  oa6v4v  933  lem3.3.4  1053  lem3.3.7i3e1  1066  vneulem3  1133  vneulem7  1137  vneulem13  1143  vneulemexp  1148