Description: Two formulations of the axiom of the empty set ax-nul . Proposal: place it right before ax-nul . (Contributed by BJ, 30-Nov-2019) (Proof modification is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | bj-nul | |- ( (/) e. _V <-> E. x A. y -. y e. x ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | isset | |- ( (/) e. _V <-> E. x 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 | bitri | |- ( (/) e. _V <-> E. x A. y -. y e. x ) |