Description: Obsolete version of 0sdomg as of 29-Nov-2024. (Contributed by NM, 23-Mar-2006) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | 0sdomgOLD | |- ( 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 | ensymb | |- ( (/) ~~ A <-> A ~~ (/) ) |
|
| 6 | en0 | |- ( A ~~ (/) <-> A = (/) ) |
|
| 7 | 5 6 | bitri | |- ( (/) ~~ A <-> A = (/) ) |
| 8 | 7 | necon3bbii | |- ( -. (/) ~~ A <-> A =/= (/) ) |
| 9 | 4 8 | bitrdi | |- ( A e. V -> ( (/) ~< A <-> A =/= (/) ) ) |