Theorem reldm0 5918

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 5782	. . 3 ⊢ Rel ∅
2		eqrel 5766	. . 3 ⊢ ((Rel 𝐴 ∧ Rel ∅) → (𝐴 = ∅ ↔ ∀𝑥∀𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ⟨𝑥, 𝑦⟩ ∈ ∅)))
3	1, 2	mpan2 704	. 2 ⊢ (Rel 𝐴 → (𝐴 = ∅ ↔ ∀𝑥∀𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ⟨𝑥, 𝑦⟩ ∈ ∅)))
4		eq0 4300	. . 3 ⊢ (dom 𝐴 = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ dom 𝐴)
5		alnex 1814	. . . . . 6 ⊢ (∀𝑦 ¬ ⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ¬ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴)
6		vex 3458	. . . . . . 7 ⊢ 𝑥 ∈ V
7	6	eldm2 5891	. . . . . 6 ⊢ (𝑥 ∈ dom 𝐴 ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴)
8	5, 7	xchbinxr 338	. . . . 5 ⊢ (∀𝑦 ¬ ⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ¬ 𝑥 ∈ dom 𝐴)
9		noel 4286	. . . . . . 7 ⊢ ¬ ⟨𝑥, 𝑦⟩ ∈ ∅
10	9	nbn 375	. . . . . 6 ⊢ (¬ ⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ (⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ⟨𝑥, 𝑦⟩ ∈ ∅))
11	10	albii 1852	. . . . 5 ⊢ (∀𝑦 ¬ ⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ∀𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ⟨𝑥, 𝑦⟩ ∈ ∅))
12	8, 11	bitr3i 280	. . . 4 ⊢ (¬ 𝑥 ∈ dom 𝐴 ↔ ∀𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ⟨𝑥, 𝑦⟩ ∈ ∅))
13	12	albii 1852	. . 3 ⊢ (∀𝑥 ¬ 𝑥 ∈ dom 𝐴 ↔ ∀𝑥∀𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ⟨𝑥, 𝑦⟩ ∈ ∅))
14	4, 13	bitr2i 279	. 2 ⊢ (∀𝑥∀𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ⟨𝑥, 𝑦⟩ ∈ ∅) ↔ dom 𝐴 = ∅)
15	3, 14	bitrdi 290	1 ⊢ (Rel 𝐴 → (𝐴 = ∅ ↔ dom 𝐴 = ∅))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209  ∀wal 1568   = wceq 1570  ∃wex 1812   ∈ wcel 2147  ∅c0 4281  ⟨cop 4838  dom cdm 5656  Rel wrel 5661

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-br 5107  df-opab 5172  df-xp 5662  df-rel 5663  df-dm 5666

This theorem is used by:  relrn0  5963  relresdm1  6038  coeq0  6271  snres0  6322  fnresdisj  6684  fn0  6695  fresaunres2  6779  funopsnOLD  7179  fsnunfv  7218  frxp  8168  frxp2  8191  frxp3  8198  domss2  9186  swrd0  14839  setsres  17388  pmtrsn  19766  gsumval3  20154  00lsp  21289  metn0  24712  noetasuplem2  28124  noetainflem2  28128  wlkn0  30234  eulerpath  30875  dfrdg2  36748  mbfresfi  38789  mapfzcons1  43932  diophrw  43974  eldioph2lem1  43975  eldioph2lem2  43976  tfsconcatb0  44549  tfsconcat0i  44550  tfsconcat0b  44551  sge0cl  47606  resinsn  50200  resinsnALT  50201