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

Theorem dm0rn0 5206
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 1599 . . . . . 6  |-  ( A. x  -.  E. y  x A y  <->  -.  E. x E. y  x A
y )
2 excom 1833 . . . . . 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 1599 . . . . 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 3772 . . . . . 6  |-  -.  x  e.  (/)
76nbn 347 . . . . 5  |-  ( -. 
E. y  x A y  <->  ( E. y  x A y  <->  x  e.  (/) ) )
87albii 1625 . . . 4  |-  ( A. x  -.  E. y  x A y  <->  A. x
( E. y  x A y  <->  x  e.  (/) ) )
9 noel 3772 . . . . . 6  |-  -.  y  e.  (/)
109nbn 347 . . . . 5  |-  ( -. 
E. x  x A y  <->  ( E. x  x A y  <->  y  e.  (/) ) )
1110albii 1625 . . . 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 2566 . . 3  |-  ( { x  |  E. y  x A y }  =  (/)  <->  A. x ( E. y  x A y  <->  x  e.  (/) ) )
14 abeq1 2566 . . 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 4996 . . 3  |-  dom  A  =  { x  |  E. y  x A y }
1716eqeq1i 2448 . 2  |-  ( dom 
A  =  (/)  <->  { x  |  E. y  x A y }  =  (/) )
18 dfrn2 5178 . . 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 1379    = wceq 1381   E.wex 1597    e. wcel 1802   {cab 2426   (/)c0 3768   class class class wbr 4434   dom cdm 4986   ran crn 4987
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-9 1806  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-sep 4555  ax-nul 4563  ax-pr 4673
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-eu 2270  df-mo 2271  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ne 2638  df-rab 2800  df-v 3095  df-dif 3462  df-un 3464  df-in 3466  df-ss 3473  df-nul 3769  df-if 3924  df-sn 4012  df-pr 4014  df-op 4018  df-br 4435  df-opab 4493  df-cnv 4994  df-dm 4996  df-rn 4997
This theorem is referenced by:  rn0  5241  relrn0  5247  imadisj  5343  ndmima  5360  rnsnn0  5461  f00  5754  f0rn0  5757  2nd0  6789  iinon  7010  onoviun  7013  onnseq  7014  map0b  7456  fodomfib  7799  intrnfi  7875  wdomtr  8001  noinfep  8076  noinfepOLD  8077  wemapwe  8139  wemapweOLD  8140  fin23lem31  8723  fin23lem40  8731  isf34lem7  8759  isf34lem6  8760  ttukeylem6  8894  fodomb  8904  rpnnen1lem4  11217  rpnnen1lem5  11218  fseqsupcl  12063  fseqsupubi  12064  ruclem11  13847  prmreclem6  14313  0ram  14412  0ram2  14413  0ramcl  14415  gsumval2  15778  ghmrn  16151  gexex  16730  gsumval3OLD  16779  gsumval3  16782  iinopn  19281  hauscmplem  19776  fbasrn  20255  alexsublem  20414  evth  21329  minveclem1  21709  minveclem3b  21713  ovollb2  21770  ovolunlem1a  21777  ovolunlem1  21778  ovoliunlem1  21783  ovoliun2  21787  ioombl1lem4  21841  uniioombllem1  21860  uniioombllem2  21862  uniioombllem6  21867  mbfsup  21941  mbfinf  21942  mbflimsup  21943  itg1climres  21991  itg2monolem1  22027  itg2mono  22030  itg2i1fseq2  22033  itg2cnlem1  22038  minvecolem1  25659  rge0scvg  27801  esumpcvgval  27954  cvmsss2  28589  fin2so  30012  heicant  30021  isbnd3  30252  totbndbnd  30257  stoweidlem35  31706
  Copyright terms: Public domain W3C validator