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

Proof

Step	Hyp	Ref	Expression
1		breq1	⊢ ( 𝑧 = 𝑥 → ( 𝑧 𝐴 𝑦 ↔ 𝑥 𝐴 𝑦 ) )
2		breq2	⊢ ( 𝑦 = 𝑤 → ( 𝑧 𝐴 𝑦 ↔ 𝑧 𝐴 𝑤 ) )
3	1 2	excomw	⊢ ( ∃ 𝑧 ∃ 𝑦 𝑧 𝐴 𝑦 ↔ ∃ 𝑦 ∃ 𝑧 𝑧 𝐴 𝑦 )
4		breq2	⊢ ( 𝑦 = 𝑤 → ( 𝑥 𝐴 𝑦 ↔ 𝑥 𝐴 𝑤 ) )
5	1 4	sylan9bbr	⊢ ( ( 𝑦 = 𝑤 ∧ 𝑧 = 𝑥 ) → ( 𝑧 𝐴 𝑦 ↔ 𝑥 𝐴 𝑤 ) )
6	5	cbvex2vw	⊢ ( ∃ 𝑦 ∃ 𝑧 𝑧 𝐴 𝑦 ↔ ∃ 𝑤 ∃ 𝑥 𝑥 𝐴 𝑤 )
7	3 6	bitri	⊢ ( ∃ 𝑧 ∃ 𝑦 𝑧 𝐴 𝑦 ↔ ∃ 𝑤 ∃ 𝑥 𝑥 𝐴 𝑤 )
8	7	notbii	⊢ ( ¬ ∃ 𝑧 ∃ 𝑦 𝑧 𝐴 𝑦 ↔ ¬ ∃ 𝑤 ∃ 𝑥 𝑥 𝐴 𝑤 )
9		alnex	⊢ ( ∀ 𝑧 ¬ ∃ 𝑦 𝑧 𝐴 𝑦 ↔ ¬ ∃ 𝑧 ∃ 𝑦 𝑧 𝐴 𝑦 )
10		alnex	⊢ ( ∀ 𝑤 ¬ ∃ 𝑥 𝑥 𝐴 𝑤 ↔ ¬ ∃ 𝑤 ∃ 𝑥 𝑥 𝐴 𝑤 )
11	8 9 10	3bitr4i	⊢ ( ∀ 𝑧 ¬ ∃ 𝑦 𝑧 𝐴 𝑦 ↔ ∀ 𝑤 ¬ ∃ 𝑥 𝑥 𝐴 𝑤 )
12		noel	⊢ ¬ 𝑧 ∈ ∅
13	12	nbn	⊢ ( ¬ ∃ 𝑦 𝑧 𝐴 𝑦 ↔ ( ∃ 𝑦 𝑧 𝐴 𝑦 ↔ 𝑧 ∈ ∅ ) )
14	13	albii	⊢ ( ∀ 𝑧 ¬ ∃ 𝑦 𝑧 𝐴 𝑦 ↔ ∀ 𝑧 ( ∃ 𝑦 𝑧 𝐴 𝑦 ↔ 𝑧 ∈ ∅ ) )
15		noel	⊢ ¬ 𝑤 ∈ ∅
16	15	nbn	⊢ ( ¬ ∃ 𝑥 𝑥 𝐴 𝑤 ↔ ( ∃ 𝑥 𝑥 𝐴 𝑤 ↔ 𝑤 ∈ ∅ ) )
17	16	albii	⊢ ( ∀ 𝑤 ¬ ∃ 𝑥 𝑥 𝐴 𝑤 ↔ ∀ 𝑤 ( ∃ 𝑥 𝑥 𝐴 𝑤 ↔ 𝑤 ∈ ∅ ) )
18	11 14 17	3bitr3i	⊢ ( ∀ 𝑧 ( ∃ 𝑦 𝑧 𝐴 𝑦 ↔ 𝑧 ∈ ∅ ) ↔ ∀ 𝑤 ( ∃ 𝑥 𝑥 𝐴 𝑤 ↔ 𝑤 ∈ ∅ ) )
19		breq1	⊢ ( 𝑥 = 𝑧 → ( 𝑥 𝐴 𝑦 ↔ 𝑧 𝐴 𝑦 ) )
20	19	exbidv	⊢ ( 𝑥 = 𝑧 → ( ∃ 𝑦 𝑥 𝐴 𝑦 ↔ ∃ 𝑦 𝑧 𝐴 𝑦 ) )
21	20	eqabcbw	⊢ ( { 𝑥 ∣ ∃ 𝑦 𝑥 𝐴 𝑦 } = ∅ ↔ ∀ 𝑧 ( ∃ 𝑦 𝑧 𝐴 𝑦 ↔ 𝑧 ∈ ∅ ) )
22	4	exbidv	⊢ ( 𝑦 = 𝑤 → ( ∃ 𝑥 𝑥 𝐴 𝑦 ↔ ∃ 𝑥 𝑥 𝐴 𝑤 ) )
23	22	eqabcbw	⊢ ( { 𝑦 ∣ ∃ 𝑥 𝑥 𝐴 𝑦 } = ∅ ↔ ∀ 𝑤 ( ∃ 𝑥 𝑥 𝐴 𝑤 ↔ 𝑤 ∈ ∅ ) )
24	18 21 23	3bitr4i	⊢ ( { 𝑥 ∣ ∃ 𝑦 𝑥 𝐴 𝑦 } = ∅ ↔ { 𝑦 ∣ ∃ 𝑥 𝑥 𝐴 𝑦 } = ∅ )
25		df-dm	⊢ dom 𝐴 = { 𝑥 ∣ ∃ 𝑦 𝑥 𝐴 𝑦 }
26	25	eqeq1i	⊢ ( dom 𝐴 = ∅ ↔ { 𝑥 ∣ ∃ 𝑦 𝑥 𝐴 𝑦 } = ∅ )
27		dfrn2	⊢ ran 𝐴 = { 𝑦 ∣ ∃ 𝑥 𝑥 𝐴 𝑦 }
28	27	eqeq1i	⊢ ( ran 𝐴 = ∅ ↔ { 𝑦 ∣ ∃ 𝑥 𝑥 𝐴 𝑦 } = ∅ )
29	24 26 28	3bitr4i	⊢ ( dom 𝐴 = ∅ ↔ ran 𝐴 = ∅ )

Metamath Proof Explorer

Theorem dm0rn0

Proof