MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  reldm0 Structured version   Visualization version   GIF version

Theorem reldm0 5544
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.
StepHypRef Expression
1 rel0 5445 . . 3 Rel ∅
2 eqrel 5411 . . 3 ((Rel 𝐴 ∧ Rel ∅) → (𝐴 = ∅ ↔ ∀𝑥𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ⟨𝑥, 𝑦⟩ ∈ ∅)))
31, 2mpan2 674 . 2 (Rel 𝐴 → (𝐴 = ∅ ↔ ∀𝑥𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ⟨𝑥, 𝑦⟩ ∈ ∅)))
4 eq0 4130 . . 3 (dom 𝐴 = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ dom 𝐴)
5 alnex 1861 . . . . . 6 (∀𝑦 ¬ ⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ¬ ∃𝑦𝑥, 𝑦⟩ ∈ 𝐴)
6 vex 3394 . . . . . . 7 𝑥 ∈ V
76eldm2 5523 . . . . . 6 (𝑥 ∈ dom 𝐴 ↔ ∃𝑦𝑥, 𝑦⟩ ∈ 𝐴)
85, 7xchbinxr 326 . . . . 5 (∀𝑦 ¬ ⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ¬ 𝑥 ∈ dom 𝐴)
9 noel 4120 . . . . . . 7 ¬ ⟨𝑥, 𝑦⟩ ∈ ∅
109nbn 363 . . . . . 6 (¬ ⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ (⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ⟨𝑥, 𝑦⟩ ∈ ∅))
1110albii 1904 . . . . 5 (∀𝑦 ¬ ⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ∀𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ⟨𝑥, 𝑦⟩ ∈ ∅))
128, 11bitr3i 268 . . . 4 𝑥 ∈ dom 𝐴 ↔ ∀𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ⟨𝑥, 𝑦⟩ ∈ ∅))
1312albii 1904 . . 3 (∀𝑥 ¬ 𝑥 ∈ dom 𝐴 ↔ ∀𝑥𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ⟨𝑥, 𝑦⟩ ∈ ∅))
144, 13bitr2i 267 . 2 (∀𝑥𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ⟨𝑥, 𝑦⟩ ∈ ∅) ↔ dom 𝐴 = ∅)
153, 14syl6bb 278 1 (Rel 𝐴 → (𝐴 = ∅ ↔ dom 𝐴 = ∅))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wal 1635   = wceq 1637  wex 1859  wcel 2156  c0 4116  cop 4376  dom cdm 5311  Rel wrel 5316
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-rab 3105  df-v 3393  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4117  df-if 4280  df-sn 4371  df-pr 4373  df-op 4377  df-br 4845  df-opab 4907  df-xp 5317  df-rel 5318  df-dm 5321
This theorem is referenced by:  relrn0  5584  coeq0  5858  fnresdisj  6212  fn0  6222  fresaunres2  6291  funopsn  6637  fsnunfv  6678  frxp  7521  domss2  8358  swrd0  13658  setsres  16112  pmtrsn  18140  gsumval3  18509  00lsp  19188  metn0  22378  wlkn0  26744  eulerpath  27414  funresdm1  29741  dfrdg2  32021  mbfresfi  33768  mapfzcons1  37782  diophrw  37824  eldioph2lem1  37825  eldioph2lem2  37826  sge0cl  41077
  Copyright terms: Public domain W3C validator