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

Theorem reldm0 5588
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 5470 . . 3 Rel ∅
2 eqrel 5456 . . 3 ((Rel 𝐴 ∧ Rel ∅) → (𝐴 = ∅ ↔ ∀𝑥𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ⟨𝑥, 𝑦⟩ ∈ ∅)))
31, 2mpan2 681 . 2 (Rel 𝐴 → (𝐴 = ∅ ↔ ∀𝑥𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ⟨𝑥, 𝑦⟩ ∈ ∅)))
4 eq0 4157 . . 3 (dom 𝐴 = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ dom 𝐴)
5 alnex 1825 . . . . . 6 (∀𝑦 ¬ ⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ¬ ∃𝑦𝑥, 𝑦⟩ ∈ 𝐴)
6 vex 3401 . . . . . . 7 𝑥 ∈ V
76eldm2 5567 . . . . . 6 (𝑥 ∈ dom 𝐴 ↔ ∃𝑦𝑥, 𝑦⟩ ∈ 𝐴)
85, 7xchbinxr 327 . . . . 5 (∀𝑦 ¬ ⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ¬ 𝑥 ∈ dom 𝐴)
9 noel 4146 . . . . . . 7 ¬ ⟨𝑥, 𝑦⟩ ∈ ∅
109nbn 364 . . . . . 6 (¬ ⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ (⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ⟨𝑥, 𝑦⟩ ∈ ∅))
1110albii 1863 . . . . 5 (∀𝑦 ¬ ⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ∀𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ⟨𝑥, 𝑦⟩ ∈ ∅))
128, 11bitr3i 269 . . . 4 𝑥 ∈ dom 𝐴 ↔ ∀𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ⟨𝑥, 𝑦⟩ ∈ ∅))
1312albii 1863 . . 3 (∀𝑥 ¬ 𝑥 ∈ dom 𝐴 ↔ ∀𝑥𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ⟨𝑥, 𝑦⟩ ∈ ∅))
144, 13bitr2i 268 . 2 (∀𝑥𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ⟨𝑥, 𝑦⟩ ∈ ∅) ↔ dom 𝐴 = ∅)
153, 14syl6bb 279 1 (Rel 𝐴 → (𝐴 = ∅ ↔ dom 𝐴 = ∅))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198  wal 1599   = wceq 1601  wex 1823  wcel 2107  c0 4141  cop 4404  dom cdm 5355  Rel wrel 5360
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-rab 3099  df-v 3400  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-nul 4142  df-if 4308  df-sn 4399  df-pr 4401  df-op 4405  df-br 4887  df-opab 4949  df-xp 5361  df-rel 5362  df-dm 5365
This theorem is referenced by:  relrn0  5629  coeq0  5898  fnresdisj  6247  fn0  6257  fresaunres2  6326  funopsn  6679  fsnunfv  6724  frxp  7568  domss2  8407  swrd0  13753  setsres  16297  pmtrsn  18323  gsumval3  18694  00lsp  19376  metn0  22573  wlkn0  26968  eulerpath  27645  funresdm1  29979  dfrdg2  32289  mbfresfi  34081  mapfzcons1  38240  diophrw  38282  eldioph2lem1  38283  eldioph2lem2  38284  sge0cl  41522
  Copyright terms: Public domain W3C validator