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 | |- U. (/) = (/) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 0ss | |- (/) C_ { (/) } |
|
| 2 | uni0b | |- ( U. (/) = (/) <-> (/) C_ { (/) } ) |
|
| 3 | 1 2 | mpbir | |- U. (/) = (/) |