Metamath Proof Explorer

Theorem reldm0

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

Ref Expression
Assertion reldm0 ⊢ Rel ⁡ A → A = ∅ ↔ dom ⁡ A = ∅

Proof

Step Hyp Ref Expression
1 rel0 ⊢ Rel ⁡ ∅
2 eqrel ⊢ Rel ⁡ A ∧ Rel ⁡ ∅ → A = ∅ ↔ ∀ x ∀ y x y ∈ A ↔ x y ∈ ∅
3 1 2 mpan2 ⊢ Rel ⁡ A → A = ∅ ↔ ∀ x ∀ y x y ∈ A ↔ x y ∈ ∅
4 eq0 ⊢ dom ⁡ A = ∅ ↔ ∀ x ¬ x ∈ dom ⁡ A
5 alnex ⊢ ∀ y ¬ x y ∈ A ↔ ¬ ∃ y x y ∈ A
6 vex ⊢ x ∈ V
7 6 eldm2 ⊢ x ∈ dom ⁡ A ↔ ∃ y x y ∈ A
8 5 7 xchbinxr ⊢ ∀ y ¬ x y ∈ A ↔ ¬ x ∈ dom ⁡ A
9 noel ⊢ ¬ x y ∈ ∅
10 9 nbn ⊢ ¬ x y ∈ A ↔ x y ∈ A ↔ x y ∈ ∅
11 10 albii ⊢ ∀ y ¬ x y ∈ A ↔ ∀ y x y ∈ A ↔ x y ∈ ∅
12 8 11 bitr3i ⊢ ¬ x ∈ dom ⁡ A ↔ ∀ y x y ∈ A ↔ x y ∈ ∅
13 12 albii ⊢ ∀ x ¬ x ∈ dom ⁡ A ↔ ∀ x ∀ y x y ∈ A ↔ x y ∈ ∅
14 4 13 bitr2i ⊢ ∀ x ∀ y x y ∈ A ↔ x y ∈ ∅ ↔ dom ⁡ A = ∅
15 3 14 bitrdi ⊢ Rel ⁡ A → A = ∅ ↔ dom ⁡ A = ∅