Theorem reldm0 5791

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

Assertion

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

Proof of Theorem reldm0

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		rel0 5665	. . 3 ⊢ Rel ∅
2		eqrel 5651	. . 3 ⊢ ((Rel 𝐴 ∧ Rel ∅) → (𝐴 = ∅ ↔ ∀𝑥∀𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ⟨𝑥, 𝑦⟩ ∈ ∅)))
3	1, 2	mpan2 689	. 2 ⊢ (Rel 𝐴 → (𝐴 = ∅ ↔ ∀𝑥∀𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ⟨𝑥, 𝑦⟩ ∈ ∅)))
4		eq0 4306	. . 3 ⊢ (dom 𝐴 = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ dom 𝐴)
5		alnex 1776	. . . . . 6 ⊢ (∀𝑦 ¬ ⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ¬ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴)
6		vex 3496	. . . . . . 7 ⊢ 𝑥 ∈ V
7	6	eldm2 5763	. . . . . 6 ⊢ (𝑥 ∈ dom 𝐴 ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴)
8	5, 7	xchbinxr 337	. . . . 5 ⊢ (∀𝑦 ¬ ⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ¬ 𝑥 ∈ dom 𝐴)
9		noel 4294	. . . . . . 7 ⊢ ¬ ⟨𝑥, 𝑦⟩ ∈ ∅
10	9	nbn 375	. . . . . 6 ⊢ (¬ ⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ (⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ⟨𝑥, 𝑦⟩ ∈ ∅))
11	10	albii 1814	. . . . 5 ⊢ (∀𝑦 ¬ ⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ∀𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ⟨𝑥, 𝑦⟩ ∈ ∅))
12	8, 11	bitr3i 279	. . . 4 ⊢ (¬ 𝑥 ∈ dom 𝐴 ↔ ∀𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ⟨𝑥, 𝑦⟩ ∈ ∅))
13	12	albii 1814	. . 3 ⊢ (∀𝑥 ¬ 𝑥 ∈ dom 𝐴 ↔ ∀𝑥∀𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ⟨𝑥, 𝑦⟩ ∈ ∅))
14	4, 13	bitr2i 278	. 2 ⊢ (∀𝑥∀𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ⟨𝑥, 𝑦⟩ ∈ ∅) ↔ dom 𝐴 = ∅)
15	3, 14	syl6bb 289	1 ⊢ (Rel 𝐴 → (𝐴 = ∅ ↔ dom 𝐴 = ∅))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208  ∀wal 1529   = wceq 1531  ∃wex 1774   ∈ wcel 2108  ∅c0 4289  ⟨cop 4565  dom cdm 5548  Rel wrel 5553

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1084  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-rab 3145  df-v 3495  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-nul 4290  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-br 5058  df-opab 5120  df-xp 5554  df-rel 5555  df-dm 5558

This theorem is referenced by:  relrn0  5833  coeq0  6101  fnresdisj  6460  fn0  6472  fresaunres2  6543  funopsn  6903  fsnunfv  6942  frxp  7812  domss2  8668  swrd0  14012  setsres  16517  pmtrsn  18639  gsumval3  19019  00lsp  19745  metn0  22962  wlkn0  27394  eulerpath  28012  funresdm1  30347  dfrdg2  33033  mbfresfi  34930  mapfzcons1  39304  diophrw  39346  eldioph2lem1  39347  eldioph2lem2  39348  sge0cl  42653