Theorem uni0

Description: The union of the empty set is the empty set. Theorem 8.7 of Quine p. 54. (Contributed by NM, 16-Sep-1993) Remove use of ax-nul . (Revised by Eric Schmidt, 4-Apr-2007)

	Ref	Expression
Assertion	uni0	⊢ ∪ ∅ = ∅

Proof

Step	Hyp	Ref	Expression
1		0ss	⊢ ∅ ⊆ { ∅ }
2		uni0b	⊢ ( ∪ ∅ = ∅ ↔ ∅ ⊆ { ∅ } )
3	1 2	mpbir	⊢ ∪ ∅ = ∅