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

Theorem reldm0 5930
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 5801 . . 3 Rel ∅
2 eqrel 5786 . . 3 ((Rel 𝐴 ∧ Rel ∅) → (𝐴 = ∅ ↔ ∀𝑥𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ⟨𝑥, 𝑦⟩ ∈ ∅)))
31, 2mpan2 689 . 2 (Rel 𝐴 → (𝐴 = ∅ ↔ ∀𝑥𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ⟨𝑥, 𝑦⟩ ∈ ∅)))
4 eq0 4343 . . 3 (dom 𝐴 = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ dom 𝐴)
5 alnex 1775 . . . . . 6 (∀𝑦 ¬ ⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ¬ ∃𝑦𝑥, 𝑦⟩ ∈ 𝐴)
6 vex 3465 . . . . . . 7 𝑥 ∈ V
76eldm2 5904 . . . . . 6 (𝑥 ∈ dom 𝐴 ↔ ∃𝑦𝑥, 𝑦⟩ ∈ 𝐴)
85, 7xchbinxr 334 . . . . 5 (∀𝑦 ¬ ⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ¬ 𝑥 ∈ dom 𝐴)
9 noel 4330 . . . . . . 7 ¬ ⟨𝑥, 𝑦⟩ ∈ ∅
109nbn 371 . . . . . 6 (¬ ⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ (⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ⟨𝑥, 𝑦⟩ ∈ ∅))
1110albii 1813 . . . . 5 (∀𝑦 ¬ ⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ∀𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ⟨𝑥, 𝑦⟩ ∈ ∅))
128, 11bitr3i 276 . . . 4 𝑥 ∈ dom 𝐴 ↔ ∀𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ⟨𝑥, 𝑦⟩ ∈ ∅))
1312albii 1813 . . 3 (∀𝑥 ¬ 𝑥 ∈ dom 𝐴 ↔ ∀𝑥𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ⟨𝑥, 𝑦⟩ ∈ ∅))
144, 13bitr2i 275 . 2 (∀𝑥𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ⟨𝑥, 𝑦⟩ ∈ ∅) ↔ dom 𝐴 = ∅)
153, 14bitrdi 286 1 (Rel 𝐴 → (𝐴 = ∅ ↔ dom 𝐴 = ∅))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wal 1531   = wceq 1533  wex 1773  wcel 2098  c0 4322  cop 4636  dom cdm 5678  Rel wrel 5683
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-rab 3419  df-v 3463  df-dif 3947  df-un 3949  df-ss 3961  df-nul 4323  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-br 5150  df-opab 5212  df-xp 5684  df-rel 5685  df-dm 5688
This theorem is referenced by:  relrn0  5972  relresdm1  6038  coeq0  6261  snres0  6304  fnresdisj  6676  fn0  6687  fresaunres2  6769  funopsn  7157  fsnunfv  7196  frxp  8131  frxp2  8149  frxp3  8156  domss2  9161  swrd0  14644  setsres  17150  pmtrsn  19486  gsumval3  19874  00lsp  20877  metn0  24310  noetasuplem2  27713  noetainflem2  27717  wlkn0  29507  eulerpath  30123  dfrdg2  35519  mbfresfi  37267  mapfzcons1  42276  diophrw  42318  eldioph2lem1  42319  eldioph2lem2  42320  tfsconcatb0  42912  tfsconcat0i  42913  tfsconcat0b  42914  sge0cl  45904
  Copyright terms: Public domain W3C validator