Theorem or0r 95

Description: Disjunction with 0.

Assertion

Ref	Expression
or0r	(0 ∪ a) = a

Proof of Theorem or0r

Step	Hyp	Ref	Expression
1		ax-a2 30	. 2 (0 ∪ a) = (a ∪ 0)
2		or0 94	. 2 (a ∪ 0) = a
3	1, 2	ax-r2 35	1 (0 ∪ a) = a

Syntax hints:   = wb 1   ∪ wo 6  0wf 10

This theorem is referenced by:  ud3lem1a 548  ud3lem1d 551  ud5lem1b 569  bi1o1a 780  bi3 821  bi4 822  mlaconj4 826  mhlemlem1 856  mhlem1 859  marsdenlem2 863  mlaconjo 868  mhcor1 870  oa6v4v 913

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

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

metamath.org