Description: A set strictly dominates the empty set iff it is not empty. (Contributed by NM, 23-Mar-2006) Avoid ax-pow , ax-un . (Revised by BTernaryTau, 29-Nov-2024)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | 0sdomg | |- ( A e. V -> ( (/) ~< A <-> A =/= (/) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 0domg | |- ( A e. V -> (/) ~<_ A ) |
|
| 2 | brsdom | |- ( (/) ~< A <-> ( (/) ~<_ A /\ -. (/) ~~ A ) ) |
|
| 3 | 2 | baib | |- ( (/) ~<_ A -> ( (/) ~< A <-> -. (/) ~~ A ) ) |
| 4 | 1 3 | syl | |- ( A e. V -> ( (/) ~< A <-> -. (/) ~~ A ) ) |
| 5 | en0r | |- ( (/) ~~ A <-> A = (/) ) |
|
| 6 | 5 | necon3bbii | |- ( -. (/) ~~ A <-> A =/= (/) ) |
| 7 | 4 6 | bitrdi | |- ( A e. V -> ( (/) ~< A <-> A =/= (/) ) ) |