Metamath Proof Explorer


Theorem dom0OLD

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 = (/) )

Proof

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 = (/) )