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 =