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

Theorem dm0rn0 4802
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 3366 . . . . . 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 3366 . . . . . 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 2355 . . 3  |-  ( { x  |  E. y  x A y }  =  (/)  <->  A. x ( E. y  x A y  <->  x  e.  (/) ) )
14 abeq1 2355 . . 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 4598 . . 3  |-  dom  A  =  { x  |  E. y  x A y }
1716eqeq1i 2260 . 2  |-  ( dom 
A  =  (/)  <->  { x  |  E. y  x A y }  =  (/) )
18 dfrn2 4775 . . 3  |-  ran  A  =  { y  |  E. x  x A y }
1918eqeq1i 2260 . 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 2239   (/)c0 3362   class class class wbr 3920   dom cdm 4580   ran crn 4581
This theorem is referenced by:  rn0  4843  relrn0  4844  imadisj  4939  ndmima  4957  rnsnn0  5045  f00  5283  2nd0  5979  iinon  6243  onoviun  6246  onnseq  6247  map0b  6692  fodomfib  7021  intrnfi  7054  wdomtr  7173  noinfep  7244  noinfepOLD  7245  wemapwe  7284  fin23lem31  7853  fin23lem40  7861  isf34lem7  7889  isf34lem6  7890  ttukeylem6  8025  fodomb  8035  rpnnen1lem4  10224  rpnnen1lem5  10225  fseqsupcl  10917  fseqsupubi  10918  ruclem11  12392  prmreclem6  12842  0ram  12941  0ram2  12942  0ramcl  12944  gsumval2  14295  ghmrn  14531  gexex  14980  gsumval3  15026  iinopn  16480  hauscmplem  16965  fbasrn  17411  alexsublem  17570  evth  18289  minveclem1  18620  minveclem3b  18624  ovollb2  18680  ovolunlem1a  18687  ovolunlem1  18688  ovoliunlem1  18693  ovoliun2  18697  ioombl1lem4  18750  uniioombllem1  18768  uniioombllem2  18770  uniioombllem6  18775  mbfsup  18851  mbfinf  18852  mbflimsup  18853  itg1climres  18901  itg2monolem1  18937  itg2mono  18940  itg2i1fseq2  18943  itg2cnlem1  18948  minvecolem1  21283  cvmsss2  22976  isbnd3  25674  totbndbnd  25679  stoweidlem35  26918
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 1926  ax-ext 2234  ax-sep 4038  ax-nul 4046  ax-pr 4108
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 1883  df-eu 2118  df-mo 2119  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-ne 2414  df-rab 2516  df-v 2729  df-dif 3081  df-un 3083  df-in 3085  df-ss 3089  df-nul 3363  df-if 3471  df-sn 3550  df-pr 3551  df-op 3553  df-br 3921  df-opab 3975  df-cnv 4596  df-dm 4598  df-rn 4599
  Copyright terms: Public domain W3C validator