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