Description: The Null Set Axiom of ZF set theory: the empty set exists. Corollary 5.16 of TakeutiZaring p. 20. For the unabbreviated version, see ax-nul . (Contributed by NM, 21-Jun-1993) (Proof shortened by Andrew Salmon, 9-Jul-2011)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | 0ex | |- (/) e. _V |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ax-nul | |- E. x A. y -. y e. x |
|
| 2 | eq0 | |- ( x = (/) <-> A. y -. y e. x ) |
|
| 3 | 2 | exbii | |- ( E. x x = (/) <-> E. x A. y -. y e. x ) |
| 4 | 1 3 | mpbir | |- E. x x = (/) |
| 5 | 4 | issetri | |- (/) e. _V |