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