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 ¬ ∃ y x A y ↔ ¬ ∃ x ∃ y x A y
2 excom ⊢ ∃ x ∃ y x A y ↔ ∃ y ∃ x x A y
3 1 2 xchbinx ⊢ ∀ x ¬ ∃ y x A y ↔ ¬ ∃ y ∃ x x A y
4 alnex ⊢ ∀ y ¬ ∃ x x A y ↔ ¬ ∃ y ∃ x x A y
5 3 4 bitr4i ⊢ ∀ x ¬ ∃ y x A y ↔ ∀ y ¬ ∃ x x A y
6 noel ⊢ ¬ x ∈ ∅
7 6 nbn ⊢ ¬ ∃ y x A y ↔ ∃ y x A y ↔ x ∈ ∅
8 7 albii ⊢ ∀ x ¬ ∃ y x A y ↔ ∀ x ∃ y x A y ↔ x ∈ ∅
9 noel ⊢ ¬ y ∈ ∅
10 9 nbn ⊢ ¬ ∃ x x A y ↔ ∃ x x A y ↔ y ∈ ∅
11 10 albii ⊢ ∀ y ¬ ∃ x x A y ↔ ∀ y ∃ x x A y ↔ y ∈ ∅
12 5 8 11 3bitr3i ⊢ ∀ x ∃ y x A y ↔ x ∈ ∅ ↔ ∀ y ∃ x x A y ↔ y ∈ ∅
13 abeq1 ⊢ x | ∃ y x A y = ∅ ↔ ∀ x ∃ y x A y ↔ x ∈ ∅
14 abeq1 ⊢ y | ∃ x x A y = ∅ ↔ ∀ y ∃ x x A y ↔ y ∈ ∅
15 12 13 14 3bitr4i ⊢ x | ∃ y x A y = ∅ ↔ y | ∃ x x A y = ∅
16 df-dm ⊢ dom ⁡ A = x | ∃ y x A y
17 16 eqeq1i ⊢ dom ⁡ A = ∅ ↔ x | ∃ y x A y = ∅
18 dfrn2 ⊢ ran ⁡ A = y | ∃ x x A y
19 18 eqeq1i ⊢ ran ⁡ A = ∅ ↔ y | ∃ x x A y = ∅
20 15 17 19 3bitr4i ⊢ dom ⁡ A = ∅ ↔ ran ⁡ A = ∅