Theorem reldm0

Description: A relation is empty iff its domain is empty. (Contributed by NM, 15-Sep-2004)

	Ref	Expression
Assertion	reldm0	⊢ ( Rel 𝐴 → ( 𝐴 = ∅ ↔ dom 𝐴 = ∅ ) )

Proof

Step	Hyp	Ref	Expression
1		rel0	⊢ Rel ∅
2		eqrel	⊢ ( ( Rel 𝐴 ∧ Rel ∅ ) → ( 𝐴 = ∅ ↔ ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ∅ ) ) )
3	1 2	mpan2	⊢ ( Rel 𝐴 → ( 𝐴 = ∅ ↔ ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ∅ ) ) )
4		eq0	⊢ ( dom 𝐴 = ∅ ↔ ∀ 𝑥 ¬ 𝑥 ∈ dom 𝐴 )
5		alnex	⊢ ( ∀ 𝑦 ¬ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ↔ ¬ ∃ 𝑦 ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 )
6		vex	⊢ 𝑥 ∈ V
7	6	eldm2	⊢ ( 𝑥 ∈ dom 𝐴 ↔ ∃ 𝑦 ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 )
8	5 7	xchbinxr	⊢ ( ∀ 𝑦 ¬ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ↔ ¬ 𝑥 ∈ dom 𝐴 )
9		noel	⊢ ¬ ⟨ 𝑥 , 𝑦 ⟩ ∈ ∅
10	9	nbn	⊢ ( ¬ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ∅ ) )
11	10	albii	⊢ ( ∀ 𝑦 ¬ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ↔ ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ∅ ) )
12	8 11	bitr3i	⊢ ( ¬ 𝑥 ∈ dom 𝐴 ↔ ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ∅ ) )
13	12	albii	⊢ ( ∀ 𝑥 ¬ 𝑥 ∈ dom 𝐴 ↔ ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ∅ ) )
14	4 13	bitr2i	⊢ ( ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ∅ ) ↔ dom 𝐴 = ∅ )
15	3 14	bitrdi	⊢ ( Rel 𝐴 → ( 𝐴 = ∅ ↔ dom 𝐴 = ∅ ) )