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∀yxy∈A↔xy∈∅
3 1 2 mpan2 ⊢Rel⁡A→A=∅↔∀x∀yxy∈A↔xy∈∅
4 eq0 ⊢dom⁡A=∅↔∀x¬x∈dom⁡A
5 alnex ⊢∀y¬xy∈A↔¬∃yxy∈A
6 vex ⊢x∈V
7 6 eldm2 ⊢x∈dom⁡A↔∃yxy∈A
8 5 7 xchbinxr ⊢∀y¬xy∈A↔¬x∈dom⁡A
9 noel ⊢¬xy∈∅
10 9 nbn ⊢¬xy∈A↔xy∈A↔xy∈∅
11 10 albii ⊢∀y¬xy∈A↔∀yxy∈A↔xy∈∅
12 8 11 bitr3i ⊢¬x∈dom⁡A↔∀yxy∈A↔xy∈∅
13 12 albii ⊢∀x¬x∈dom⁡A↔∀x∀yxy∈A↔xy∈∅
14 4 13 bitr2i ⊢∀x∀yxy∈A↔xy∈∅↔dom⁡A=∅
15 3 14 bitrdi ⊢Rel⁡A→A=∅↔dom⁡A=∅