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

Theorem dm0rn0 5224
Description: An empty domain implies an empty range. (Contributed by NM, 21-May-1998.)
Assertion
Ref Expression
dm0rn0

Proof of Theorem dm0rn0
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 alnex 1614 . . . . . 6
2 excom 1849 . . . . . 6
31, 2xchbinx 310 . . . . 5
4 alnex 1614 . . . . 5
53, 4bitr4i 252 . . . 4
6 noel 3788 . . . . . 6
76nbn 347 . . . . 5
87albii 1640 . . . 4
9 noel 3788 . . . . . 6
109nbn 347 . . . . 5
1110albii 1640 . . . 4
125, 8, 113bitr3i 275 . . 3
13 abeq1 2582 . . 3
14 abeq1 2582 . . 3
1512, 13, 143bitr4i 277 . 2
16 df-dm 5014 . . 3
1716eqeq1i 2464 . 2
18 dfrn2 5196 . . 3
1918eqeq1i 2464 . 2
2015, 17, 193bitr4i 277 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  <->wb 184  A.wal 1393  =wceq 1395  E.wex 1612  e.wcel 1818  {cab 2442   c0 3784   class class class wbr 4452  domcdm 5004  rancrn 5005
This theorem is referenced by:  rn0  5259  relrn0  5265  imadisj  5361  ndmima  5378  rnsnn0  5479  f00  5772  f0rn0  5775  2nd0  6807  iinon  7030  onoviun  7033  onnseq  7034  map0b  7477  fodomfib  7820  intrnfi  7896  wdomtr  8022  noinfep  8097  noinfepOLD  8098  wemapwe  8160  wemapweOLD  8161  fin23lem31  8744  fin23lem40  8752  isf34lem7  8780  isf34lem6  8781  ttukeylem6  8915  fodomb  8925  rpnnen1lem4  11240  rpnnen1lem5  11241  fseqsupcl  12087  fseqsupubi  12088  ruclem11  13973  prmreclem6  14439  0ram  14538  0ram2  14539  0ramcl  14541  gsumval2  15907  ghmrn  16280  gexex  16859  gsumval3OLD  16908  gsumval3  16911  iinopn  19411  hauscmplem  19906  fbasrn  20385  alexsublem  20544  evth  21459  minveclem1  21839  minveclem3b  21843  ovollb2  21900  ovolunlem1a  21907  ovolunlem1  21908  ovoliunlem1  21913  ovoliun2  21917  ioombl1lem4  21971  uniioombllem1  21990  uniioombllem2  21992  uniioombllem6  21997  mbfsup  22071  mbfinf  22072  mbflimsup  22073  itg1climres  22121  itg2monolem1  22157  itg2mono  22160  itg2i1fseq2  22163  itg2cnlem1  22168  minvecolem1  25790  rge0scvg  27931  esumpcvgval  28084  cvmsss2  28719  fin2so  30040  heicant  30049  isbnd3  30280  totbndbnd  30285  stoweidlem35  31817
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pr 4691
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-br 4453  df-opab 4511  df-cnv 5012  df-dm 5014  df-rn 5015
  Copyright terms: Public domain W3C validator