This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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