Metamath Proof Explorer

Theorem dm0rn0

Description: An empty domain is equivalent to an empty range. (Contributed by NM, 21-May-1998)

Ref Expression
Assertion dm0rn0 ⊢dom⁡A=∅↔ran⁡A=∅

Proof

Step Hyp Ref Expression
1 alnex ⊢∀x¬∃yxAy↔¬∃x∃yxAy
2 excom ⊢∃x∃yxAy↔∃y∃xxAy
3 1 2 xchbinx ⊢∀x¬∃yxAy↔¬∃y∃xxAy
4 alnex ⊢∀y¬∃xxAy↔¬∃y∃xxAy
5 3 4 bitr4i ⊢∀x¬∃yxAy↔∀y¬∃xxAy
6 noel ⊢¬x∈∅
7 6 nbn ⊢¬∃yxAy↔∃yxAy↔x∈∅
8 7 albii ⊢∀x¬∃yxAy↔∀x∃yxAy↔x∈∅
9 noel ⊢¬y∈∅
10 9 nbn ⊢¬∃xxAy↔∃xxAy↔y∈∅
11 10 albii ⊢∀y¬∃xxAy↔∀y∃xxAy↔y∈∅
12 5 8 11 3bitr3i ⊢∀x∃yxAy↔x∈∅↔∀y∃xxAy↔y∈∅
13 eqabcb ⊢x|∃yxAy=∅↔∀x∃yxAy↔x∈∅
14 eqabcb ⊢y|∃xxAy=∅↔∀y∃xxAy↔y∈∅
15 12 13 14 3bitr4i ⊢x|∃yxAy=∅↔y|∃xxAy=∅
16 df-dm ⊢dom⁡A=x|∃yxAy
17 16 eqeq1i ⊢dom⁡A=∅↔x|∃yxAy=∅
18 dfrn2 ⊢ran⁡A=y|∃xxAy
19 18 eqeq1i ⊢ran⁡A=∅↔y|∃xxAy=∅
20 15 17 19 3bitr4i ⊢dom⁡A=∅↔ran⁡A=∅