# 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 𝐴 = ∅ ↔ ran 𝐴 = ∅ )

### Proof

Step Hyp Ref Expression
1 alnex ( ∀ 𝑥 ¬ ∃ 𝑦 𝑥 𝐴 𝑦 ↔ ¬ ∃ 𝑥𝑦 𝑥 𝐴 𝑦 )
2 excom ( ∃ 𝑥𝑦 𝑥 𝐴 𝑦 ↔ ∃ 𝑦𝑥 𝑥 𝐴 𝑦 )
3 1 2 xchbinx ( ∀ 𝑥 ¬ ∃ 𝑦 𝑥 𝐴 𝑦 ↔ ¬ ∃ 𝑦𝑥 𝑥 𝐴 𝑦 )
4 alnex ( ∀ 𝑦 ¬ ∃ 𝑥 𝑥 𝐴 𝑦 ↔ ¬ ∃ 𝑦𝑥 𝑥 𝐴 𝑦 )
5 3 4 bitr4i ( ∀ 𝑥 ¬ ∃ 𝑦 𝑥 𝐴 𝑦 ↔ ∀ 𝑦 ¬ ∃ 𝑥 𝑥 𝐴 𝑦 )
6 noel ¬ 𝑥 ∈ ∅
7 6 nbn ( ¬ ∃ 𝑦 𝑥 𝐴 𝑦 ↔ ( ∃ 𝑦 𝑥 𝐴 𝑦𝑥 ∈ ∅ ) )
8 7 albii ( ∀ 𝑥 ¬ ∃ 𝑦 𝑥 𝐴 𝑦 ↔ ∀ 𝑥 ( ∃ 𝑦 𝑥 𝐴 𝑦𝑥 ∈ ∅ ) )
9 noel ¬ 𝑦 ∈ ∅
10 9 nbn ( ¬ ∃ 𝑥 𝑥 𝐴 𝑦 ↔ ( ∃ 𝑥 𝑥 𝐴 𝑦𝑦 ∈ ∅ ) )
11 10 albii ( ∀ 𝑦 ¬ ∃ 𝑥 𝑥 𝐴 𝑦 ↔ ∀ 𝑦 ( ∃ 𝑥 𝑥 𝐴 𝑦𝑦 ∈ ∅ ) )
12 5 8 11 3bitr3i ( ∀ 𝑥 ( ∃ 𝑦 𝑥 𝐴 𝑦𝑥 ∈ ∅ ) ↔ ∀ 𝑦 ( ∃ 𝑥 𝑥 𝐴 𝑦𝑦 ∈ ∅ ) )
13 abeq1 ( { 𝑥 ∣ ∃ 𝑦 𝑥 𝐴 𝑦 } = ∅ ↔ ∀ 𝑥 ( ∃ 𝑦 𝑥 𝐴 𝑦𝑥 ∈ ∅ ) )
14 abeq1 ( { 𝑦 ∣ ∃ 𝑥 𝑥 𝐴 𝑦 } = ∅ ↔ ∀ 𝑦 ( ∃ 𝑥 𝑥 𝐴 𝑦𝑦 ∈ ∅ ) )
15 12 13 14 3bitr4i ( { 𝑥 ∣ ∃ 𝑦 𝑥 𝐴 𝑦 } = ∅ ↔ { 𝑦 ∣ ∃ 𝑥 𝑥 𝐴 𝑦 } = ∅ )
16 df-dm dom 𝐴 = { 𝑥 ∣ ∃ 𝑦 𝑥 𝐴 𝑦 }
17 16 eqeq1i ( dom 𝐴 = ∅ ↔ { 𝑥 ∣ ∃ 𝑦 𝑥 𝐴 𝑦 } = ∅ )
18 dfrn2 ran 𝐴 = { 𝑦 ∣ ∃ 𝑥 𝑥 𝐴 𝑦 }
19 18 eqeq1i ( ran 𝐴 = ∅ ↔ { 𝑦 ∣ ∃ 𝑥 𝑥 𝐴 𝑦 } = ∅ )
20 15 17 19 3bitr4i ( dom 𝐴 = ∅ ↔ ran 𝐴 = ∅ )