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

Theorem dm0rn0 4894
Description: An empty domain implies an empty range. (Contributed by NM, 21-May-1998.)
Assertion
Ref Expression
dm0rn0  |-  ( dom 
A  =  (/)  <->  ran  A  =  (/) )
Dummy variables  x  y are mutually distinct and distinct from all other variables.

Proof of Theorem dm0rn0
StepHypRef Expression
1 alnex 1531 . . . . . 6  |-  ( A. x  -.  E. y  x A y  <->  -.  E. x E. y  x A
y )
2 excom 1787 . . . . . 6  |-  ( E. x E. y  x A y  <->  E. y E. x  x A
y )
31, 2xchbinx 303 . . . . 5  |-  ( A. x  -.  E. y  x A y  <->  -.  E. y E. x  x A
y )
4 alnex 1531 . . . . 5  |-  ( A. y  -.  E. x  x A y  <->  -.  E. y E. x  x A
y )
53, 4bitr4i 245 . . . 4  |-  ( A. x  -.  E. y  x A y  <->  A. y  -.  E. x  x A y )
6 noel 3460 . . . . . 6  |-  -.  x  e.  (/)
76nbn 338 . . . . 5  |-  ( -. 
E. y  x A y  <->  ( E. y  x A y  <->  x  e.  (/) ) )
87albii 1554 . . . 4  |-  ( A. x  -.  E. y  x A y  <->  A. x
( E. y  x A y  <->  x  e.  (/) ) )
9 noel 3460 . . . . . 6  |-  -.  y  e.  (/)
109nbn 338 . . . . 5  |-  ( -. 
E. x  x A y  <->  ( E. x  x A y  <->  y  e.  (/) ) )
1110albii 1554 . . . 4  |-  ( A. y  -.  E. x  x A y  <->  A. y
( E. x  x A y  <->  y  e.  (/) ) )
125, 8, 113bitr3i 268 . . 3  |-  ( A. x ( E. y  x A y  <->  x  e.  (/) )  <->  A. y ( E. x  x A y  <-> 
y  e.  (/) ) )
13 abeq1 2390 . . 3  |-  ( { x  |  E. y  x A y }  =  (/)  <->  A. x ( E. y  x A y  <->  x  e.  (/) ) )
14 abeq1 2390 . . 3  |-  ( { y  |  E. x  x A y }  =  (/)  <->  A. y ( E. x  x A y  <->  y  e.  (/) ) )
1512, 13, 143bitr4i 270 . 2  |-  ( { x  |  E. y  x A y }  =  (/)  <->  { y  |  E. x  x A y }  =  (/) )
16 df-dm 4698 . . 3  |-  dom  A  =  { x  |  E. y  x A y }
1716eqeq1i 2291 . 2  |-  ( dom 
A  =  (/)  <->  { x  |  E. y  x A y }  =  (/) )
18 dfrn2 4867 . . 3  |-  ran  A  =  { y  |  E. x  x A y }
1918eqeq1i 2291 . 2  |-  ( ran 
A  =  (/)  <->  { y  |  E. x  x A y }  =  (/) )
2015, 17, 193bitr4i 270 1  |-  ( dom 
A  =  (/)  <->  ran  A  =  (/) )
Colors of variables: wff set class
Syntax hints:   -. wn 5    <-> wb 178   A.wal 1528   E.wex 1529    = wceq 1624    e. wcel 1685   {cab 2270   (/)c0 3456   class class class wbr 4024   dom cdm 4688   ran crn 4689
This theorem is referenced by:  rn0  4935  relrn0  4936  imadisj  5031  ndmima  5049  rnsnn0  5137  f00  5391  2nd0  6088  iinon  6352  onoviun  6355  onnseq  6356  map0b  6801  fodomfib  7131  intrnfi  7165  wdomtr  7284  noinfep  7355  noinfepOLD  7356  wemapwe  7395  fin23lem31  7964  fin23lem40  7972  isf34lem7  8000  isf34lem6  8001  ttukeylem6  8136  fodomb  8146  rpnnen1lem4  10340  rpnnen1lem5  10341  fseqsupcl  11033  fseqsupubi  11034  ruclem11  12512  prmreclem6  12962  0ram  13061  0ram2  13062  0ramcl  13064  gsumval2  14454  ghmrn  14690  gexex  15139  gsumval3  15185  iinopn  16642  hauscmplem  17127  fbasrn  17573  alexsublem  17732  evth  18451  minveclem1  18782  minveclem3b  18786  ovollb2  18842  ovolunlem1a  18849  ovolunlem1  18850  ovoliunlem1  18855  ovoliun2  18859  ioombl1lem4  18912  uniioombllem1  18930  uniioombllem2  18932  uniioombllem6  18937  mbfsup  19013  mbfinf  19014  mbflimsup  19015  itg1climres  19063  itg2monolem1  19099  itg2mono  19102  itg2i1fseq2  19105  itg2cnlem1  19110  minvecolem1  21445  cvmsss2  23209  isbnd3  25907  totbndbnd  25912  stoweidlem35  27183
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-14 1689  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1867  ax-ext 2265  ax-sep 4142  ax-nul 4150  ax-pr 4213
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 938  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-eu 2148  df-mo 2149  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-ne 2449  df-rab 2553  df-v 2791  df-dif 3156  df-un 3158  df-in 3160  df-ss 3167  df-nul 3457  df-if 3567  df-sn 3647  df-pr 3648  df-op 3650  df-br 4025  df-opab 4079  df-cnv 4696  df-dm 4698  df-rn 4699
  Copyright terms: Public domain W3C validator