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

Theorem reldm0 4912
Description: A relation is empty iff its domain is empty. (Contributed by NM, 15-Sep-2004.)
Assertion
Ref Expression
reldm0  |-  ( Rel 
A  ->  ( A  =  (/)  <->  dom  A  =  (/) ) )

Proof of Theorem reldm0
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 rel0 4826 . . 3  |-  Rel  (/)
2 eqrel 4793 . . 3  |-  ( ( Rel  A  /\  Rel  (/) )  ->  ( A  =  (/)  <->  A. x A. y
( <. x ,  y
>.  e.  A  <->  <. x ,  y >.  e.  (/) ) ) )
31, 2mpan2 652 . 2  |-  ( Rel 
A  ->  ( A  =  (/)  <->  A. x A. y
( <. x ,  y
>.  e.  A  <->  <. x ,  y >.  e.  (/) ) ) )
4 eq0 3482 . . 3  |-  ( dom 
A  =  (/)  <->  A. x  -.  x  e.  dom  A )
5 alnex 1533 . . . . . 6  |-  ( A. y  -.  <. x ,  y
>.  e.  A  <->  -.  E. y <. x ,  y >.  e.  A )
6 vex 2804 . . . . . . 7  |-  x  e. 
_V
76eldm2 4893 . . . . . 6  |-  ( x  e.  dom  A  <->  E. y <. x ,  y >.  e.  A )
85, 7xchbinxr 302 . . . . 5  |-  ( A. y  -.  <. x ,  y
>.  e.  A  <->  -.  x  e.  dom  A )
9 noel 3472 . . . . . . 7  |-  -.  <. x ,  y >.  e.  (/)
109nbn 336 . . . . . 6  |-  ( -. 
<. x ,  y >.  e.  A  <->  ( <. x ,  y >.  e.  A  <->  <.
x ,  y >.  e.  (/) ) )
1110albii 1556 . . . . 5  |-  ( A. y  -.  <. x ,  y
>.  e.  A  <->  A. y
( <. x ,  y
>.  e.  A  <->  <. x ,  y >.  e.  (/) ) )
128, 11bitr3i 242 . . . 4  |-  ( -.  x  e.  dom  A  <->  A. y ( <. x ,  y >.  e.  A  <->  <.
x ,  y >.  e.  (/) ) )
1312albii 1556 . . 3  |-  ( A. x  -.  x  e.  dom  A  <->  A. x A. y (
<. x ,  y >.  e.  A  <->  <. x ,  y
>.  e.  (/) ) )
144, 13bitr2i 241 . 2  |-  ( A. x A. y ( <.
x ,  y >.  e.  A  <->  <. x ,  y
>.  e.  (/) )  <->  dom  A  =  (/) )
153, 14syl6bb 252 1  |-  ( Rel 
A  ->  ( A  =  (/)  <->  dom  A  =  (/) ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176   A.wal 1530   E.wex 1531    = wceq 1632    e. wcel 1696   (/)c0 3468   <.cop 3656   dom cdm 4705   Rel wrel 4710
This theorem is referenced by:  relrn0  4953  fnresdisj  5370  fn0  5379  fresaunres2  5429  fsnunfv  5736  frxp  6241  domss2  7036  setsres  13190  gsumval3  15207  00lsp  15754  metn0  17940  eupath  23920  dfrdg2  24223  mapfzcons1  26897  coeq0  26934  diophrw  26941  eldioph2lem1  26942  eldioph2lem2  26943
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-14 1700  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-sep 4157  ax-nul 4165  ax-pr 4230
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-rab 2565  df-v 2803  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-br 4040  df-opab 4094  df-xp 4711  df-rel 4712  df-dm 4715
  Copyright terms: Public domain W3C validator