Description: Obsolete version of dom0 as of 29-Nov-2024. (Contributed by NM, 22-Nov-2004) (Proof modification is discouraged.) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | dom0OLD | |- ( 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 = (/) ) |