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

Theorem mpt0 5713
Description: A mapping operation with empty domain. (Contributed by Mario Carneiro, 28-Dec-2014.)
Assertion
Ref Expression
mpt0

Proof of Theorem mpt0
StepHypRef Expression
1 ral0 3934 . . 3
2 eqid 2457 . . . 4
32fnmpt 5712 . . 3
41, 3ax-mp 5 . 2
5 fn0 5705 . 2
64, 5mpbi 208 1
Colors of variables: wff setvar class
Syntax hints:  =wceq 1395  e.wcel 1818  A.wral 2807   cvv 3109   c0 3784  e.cmpt 4510  Fnwfn 5588
This theorem is referenced by:  oarec  7230  swrd00  12645  swrdlend  12656  repswswrd  12756  0rest  14827  grpinvfval  16088  psgnfval  16525  odfval  16557  gsumconst  16954  gsum2dlem2  16998  gsum2dOLD  17000  dprd0  17078  staffval  17496  asclfval  17983  mplcoe1  18127  mplcoe5  18131  mplcoe2OLD  18133  coe1fzgsumd  18344  evl1gsumd  18393  gsumfsum  18484  pjfval  18737  mavmul0  19054  submafval  19081  mdetfval  19088  nfimdetndef  19091  mdetfval1  19092  mdet0pr  19094  madufval  19139  madugsum  19145  minmar1fval  19148  cramer0  19192  nmfval  21109  mdegfval  22460  gsumvsca1  27773  gsumvsca2  27774  esumnul  28059  sitg0  28288  mrsubfval  28868  msubfval  28884  elmsubrn  28888  mvhfval  28893  msrfval  28897  cncfiooicc  31697  itgvol0  31767  stoweidlem9  31791  lincval0  33016
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-ral 2812  df-rex 2813  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-mpt 4512  df-id 4800  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-fun 5595  df-fn 5596
  Copyright terms: Public domain W3C validator