Description: A set dominated by the empty set is empty. (Contributed by NM, 22-Nov-2004)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | dom0 | |- ( A ~<_ (/) <-> A = (/) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | reldom | |- Rel ~<_ |
|
| 2 | 1 | brrelex1i | |- ( A ~<_ (/) -> A e. _V ) |
| 3 | 0domg | |- ( A e. _V -> (/) ~<_ A ) |
|
| 4 | 2 3 | syl | |- ( A ~<_ (/) -> (/) ~<_ A ) |
| 5 | 4 | pm4.71i | |- ( A ~<_ (/) <-> ( A ~<_ (/) /\ (/) ~<_ A ) ) |
| 6 | sbthb | |- ( ( A ~<_ (/) /\ (/) ~<_ A ) <-> A ~~ (/) ) |
|
| 7 | en0 | |- ( A ~~ (/) <-> A = (/) ) |
|
| 8 | 5 6 7 | 3bitri | |- ( A ~<_ (/) <-> A = (/) ) |