This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dm0rn0OLD

Description: Obsolete version of dm0rn0 as of 24-Jan-2026. (Contributed by NM, 21-May-1998) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion dm0rn0OLD ( 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 eqabcb ⊢ ( { 𝑥 ∣ ∃ 𝑦 𝑥 𝐴 𝑦 } = ∅ ↔ ∀ 𝑥 ( ∃ 𝑦 𝑥 𝐴 𝑦 ↔ 𝑥 ∈ ∅ ) )
14 eqabcb ⊢ ( { 𝑦 ∣ ∃ 𝑥 𝑥 𝐴 𝑦 } = ∅ ↔ ∀ 𝑦 ( ∃ 𝑥 𝑥 𝐴 𝑦 ↔ 𝑦 ∈ ∅ ) )
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 𝐴 = ∅ )