Metamath Proof Explorer


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 ∅ = ∅