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

Theorem dm0rn0 4869
Description: An empty domain implies an empty range. (Contributed by NM, 21-May-1998.)
Assertion
Ref Expression
dm0rn0  |-  ( dom 
A  =  (/)  <->  ran  A  =  (/) )

Proof of Theorem dm0rn0
StepHypRef Expression
1 alnex 1569 . . . . . 6  |-  ( A. x  -.  E. y  x A y  <->  -.  E. x E. y  x A
y )
2 excom 1765 . . . . . 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 1569 . . . . 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 3420 . . . . . 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 3420 . . . . . 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 2362 . . 3  |-  ( { x  |  E. y  x A y }  =  (/)  <->  A. x ( E. y  x A y  <->  x  e.  (/) ) )
14 abeq1 2362 . . 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 4665 . . 3  |-  dom  A  =  { x  |  E. y  x A y }
1716eqeq1i 2263 . 2  |-  ( dom 
A  =  (/)  <->  { x  |  E. y  x A y }  =  (/) )
18 dfrn2 4842 . . 3  |-  ran  A  =  { y  |  E. x  x A y }
1918eqeq1i 2263 . 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 1532   E.wex 1537    = wceq 1619    e. wcel 1621   {cab 2242   (/)c0 3416   class class class wbr 3983   dom cdm 4647   ran crn 4648
This theorem is referenced by:  rn0  4910  relrn0  4911  imadisj  5006  ndmima  5024  rnsnn0  5112  f00  5350  2nd0  6047  iinon  6311  onoviun  6314  onnseq  6315  map0b  6760  fodomfib  7090  intrnfi  7124  wdomtr  7243  noinfep  7314  noinfepOLD  7315  wemapwe  7354  fin23lem31  7923  fin23lem40  7931  isf34lem7  7959  isf34lem6  7960  ttukeylem6  8095  fodomb  8105  rpnnen1lem4  10298  rpnnen1lem5  10299  fseqsupcl  10991  fseqsupubi  10992  ruclem11  12466  prmreclem6  12916  0ram  13015  0ram2  13016  0ramcl  13018  gsumval2  14408  ghmrn  14644  gexex  15093  gsumval3  15139  iinopn  16596  hauscmplem  17081  fbasrn  17527  alexsublem  17686  evth  18405  minveclem1  18736  minveclem3b  18740  ovollb2  18796  ovolunlem1a  18803  ovolunlem1  18804  ovoliunlem1  18809  ovoliun2  18813  ioombl1lem4  18866  uniioombllem1  18884  uniioombllem2  18886  uniioombllem6  18891  mbfsup  18967  mbfinf  18968  mbflimsup  18969  itg1climres  19017  itg2monolem1  19053  itg2mono  19056  itg2i1fseq2  19059  itg2cnlem1  19064  minvecolem1  21399  cvmsss2  23163  isbnd3  25861  totbndbnd  25866  stoweidlem35  27105
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-14 1626  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2237  ax-sep 4101  ax-nul 4109  ax-pr 4172
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 941  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-eu 2121  df-mo 2122  df-clab 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-ne 2421  df-rab 2525  df-v 2759  df-dif 3116  df-un 3118  df-in 3120  df-ss 3127  df-nul 3417  df-if 3526  df-sn 3606  df-pr 3607  df-op 3609  df-br 3984  df-opab 4038  df-cnv 4663  df-dm 4665  df-rn 4666
  Copyright terms: Public domain W3C validator