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

Theorem dm0rn0 5054
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
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 alnex 1588 . . . . . 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 310 . . . . 5  |-  ( A. x  -.  E. y  x A y  <->  -.  E. y E. x  x A
y )
4 alnex 1588 . . . . 5  |-  ( A. y  -.  E. x  x A y  <->  -.  E. y E. x  x A
y )
53, 4bitr4i 252 . . . 4  |-  ( A. x  -.  E. y  x A y  <->  A. y  -.  E. x  x A y )
6 noel 3639 . . . . . 6  |-  -.  x  e.  (/)
76nbn 347 . . . . 5  |-  ( -. 
E. y  x A y  <->  ( E. y  x A y  <->  x  e.  (/) ) )
87albii 1610 . . . 4  |-  ( A. x  -.  E. y  x A y  <->  A. x
( E. y  x A y  <->  x  e.  (/) ) )
9 noel 3639 . . . . . 6  |-  -.  y  e.  (/)
109nbn 347 . . . . 5  |-  ( -. 
E. x  x A y  <->  ( E. x  x A y  <->  y  e.  (/) ) )
1110albii 1610 . . . 4  |-  ( A. y  -.  E. x  x A y  <->  A. y
( E. x  x A y  <->  y  e.  (/) ) )
125, 8, 113bitr3i 275 . . 3  |-  ( A. x ( E. y  x A y  <->  x  e.  (/) )  <->  A. y ( E. x  x A y  <-> 
y  e.  (/) ) )
13 abeq1 2547 . . 3  |-  ( { x  |  E. y  x A y }  =  (/)  <->  A. x ( E. y  x A y  <->  x  e.  (/) ) )
14 abeq1 2547 . . 3  |-  ( { y  |  E. x  x A y }  =  (/)  <->  A. y ( E. x  x A y  <->  y  e.  (/) ) )
1512, 13, 143bitr4i 277 . 2  |-  ( { x  |  E. y  x A y }  =  (/)  <->  { y  |  E. x  x A y }  =  (/) )
16 df-dm 4848 . . 3  |-  dom  A  =  { x  |  E. y  x A y }
1716eqeq1i 2448 . 2  |-  ( dom 
A  =  (/)  <->  { x  |  E. y  x A y }  =  (/) )
18 dfrn2 5026 . . 3  |-  ran  A  =  { y  |  E. x  x A y }
1918eqeq1i 2448 . 2  |-  ( ran 
A  =  (/)  <->  { y  |  E. x  x A y }  =  (/) )
2015, 17, 193bitr4i 277 1  |-  ( dom 
A  =  (/)  <->  ran  A  =  (/) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    <-> wb 184   A.wal 1367    = wceq 1369   E.wex 1586    e. wcel 1756   {cab 2427   (/)c0 3635   class class class wbr 4290   dom cdm 4838   ran crn 4839
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2422  ax-sep 4411  ax-nul 4419  ax-pr 4529
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-rab 2722  df-v 2972  df-dif 3329  df-un 3331  df-in 3333  df-ss 3340  df-nul 3636  df-if 3790  df-sn 3876  df-pr 3878  df-op 3882  df-br 4291  df-opab 4349  df-cnv 4846  df-dm 4848  df-rn 4849
This theorem is referenced by:  rn0  5089  relrn0  5095  imadisj  5186  ndmima  5203  rnsnn0  5303  f00  5591  2nd0  6582  iinon  6799  onoviun  6802  onnseq  6803  map0b  7249  fodomfib  7589  intrnfi  7664  wdomtr  7788  noinfep  7863  noinfepOLD  7864  wemapwe  7926  wemapweOLD  7927  fin23lem31  8510  fin23lem40  8518  isf34lem7  8546  isf34lem6  8547  ttukeylem6  8681  fodomb  8691  rpnnen1lem4  10980  rpnnen1lem5  10981  fseqsupcl  11797  fseqsupubi  11798  ruclem11  13520  prmreclem6  13980  0ram  14079  0ram2  14080  0ramcl  14082  gsumval2  15511  ghmrn  15758  gexex  16333  gsumval3OLD  16380  gsumval3  16383  iinopn  18513  hauscmplem  19007  fbasrn  19455  alexsublem  19614  evth  20529  minveclem1  20909  minveclem3b  20913  ovollb2  20970  ovolunlem1a  20977  ovolunlem1  20978  ovoliunlem1  20983  ovoliun2  20987  ioombl1lem4  21040  uniioombllem1  21059  uniioombllem2  21061  uniioombllem6  21066  mbfsup  21140  mbfinf  21141  mbflimsup  21142  itg1climres  21190  itg2monolem1  21226  itg2mono  21229  itg2i1fseq2  21232  itg2cnlem1  21237  minvecolem1  24273  rge0scvg  26377  esumpcvgval  26525  cvmsss2  27161  fin2so  28413  heicant  28423  isbnd3  28680  totbndbnd  28685  stoweidlem35  29827  f0rn0  30138
  Copyright terms: Public domain W3C validator