Metamath Proof Explorer

Theorem dm0rn0

Description: An empty domain is equivalent to an empty range. (Contributed by NM, 21-May-1998) Avoid ax-10 , ax-11 , ax-12 . (Revised by TM, 24-Jan-2026)

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

Proof

Step Hyp Ref Expression
1 breq1 ⊢ z = x → z A y ↔ x A y
2 breq2 ⊢ y = w → z A y ↔ z A w
3 1 2 excomw ⊢ ∃ z ∃ y z A y ↔ ∃ y ∃ z z A y
4 breq2 ⊢ y = w → x A y ↔ x A w
5 1 4 sylan9bbr ⊢ y = w ∧ z = x → z A y ↔ x A w
6 5 cbvex2vw ⊢ ∃ y ∃ z z A y ↔ ∃ w ∃ x x A w
7 3 6 bitri ⊢ ∃ z ∃ y z A y ↔ ∃ w ∃ x x A w
8 7 notbii ⊢ ¬ ∃ z ∃ y z A y ↔ ¬ ∃ w ∃ x x A w
9 alnex ⊢ ∀ z ¬ ∃ y z A y ↔ ¬ ∃ z ∃ y z A y
10 alnex ⊢ ∀ w ¬ ∃ x x A w ↔ ¬ ∃ w ∃ x x A w
11 8 9 10 3bitr4i ⊢ ∀ z ¬ ∃ y z A y ↔ ∀ w ¬ ∃ x x A w
12 noel ⊢ ¬ z ∈ ∅
13 12 nbn ⊢ ¬ ∃ y z A y ↔ ∃ y z A y ↔ z ∈ ∅
14 13 albii ⊢ ∀ z ¬ ∃ y z A y ↔ ∀ z ∃ y z A y ↔ z ∈ ∅
15 noel ⊢ ¬ w ∈ ∅
16 15 nbn ⊢ ¬ ∃ x x A w ↔ ∃ x x A w ↔ w ∈ ∅
17 16 albii ⊢ ∀ w ¬ ∃ x x A w ↔ ∀ w ∃ x x A w ↔ w ∈ ∅
18 11 14 17 3bitr3i ⊢ ∀ z ∃ y z A y ↔ z ∈ ∅ ↔ ∀ w ∃ x x A w ↔ w ∈ ∅
19 breq1 ⊢ x = z → x A y ↔ z A y
20 19 exbidv ⊢ x = z → ∃ y x A y ↔ ∃ y z A y
21 20 eqabcbw ⊢ x | ∃ y x A y = ∅ ↔ ∀ z ∃ y z A y ↔ z ∈ ∅
22 4 exbidv ⊢ y = w → ∃ x x A y ↔ ∃ x x A w
23 22 eqabcbw ⊢ y | ∃ x x A y = ∅ ↔ ∀ w ∃ x x A w ↔ w ∈ ∅
24 18 21 23 3bitr4i ⊢ x | ∃ y x A y = ∅ ↔ y | ∃ x x A y = ∅
25 df-dm ⊢ dom ⁡ A = x | ∃ y x A y
26 25 eqeq1i ⊢ dom ⁡ A = ∅ ↔ x | ∃ y x A y = ∅
27 dfrn2 ⊢ ran ⁡ A = y | ∃ x x A y
28 27 eqeq1i ⊢ ran ⁡ A = ∅ ↔ y | ∃ x x A y = ∅
29 24 26 28 3bitr4i ⊢ dom ⁡ A = ∅ ↔ ran ⁡ A = ∅