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

Theorem mpt0 5722
Description: A mapping operation with empty domain. (Contributed by Mario Carneiro, 28-Dec-2014.)
Assertion
Ref Expression
mpt0  |-  ( x  e.  (/)  |->  A )  =  (/)

Proof of Theorem mpt0
StepHypRef Expression
1 ral0 3904 . . 3  |-  A. x  e.  (/)  A  e.  _V
2 eqid 2423 . . . 4  |-  ( x  e.  (/)  |->  A )  =  ( x  e.  (/)  |->  A )
32fnmpt 5721 . . 3  |-  ( A. x  e.  (/)  A  e. 
_V  ->  ( x  e.  (/)  |->  A )  Fn  (/) )
41, 3ax-mp 5 . 2  |-  ( x  e.  (/)  |->  A )  Fn  (/)
5 fn0 5712 . 2  |-  ( ( x  e.  (/)  |->  A )  Fn  (/)  <->  ( x  e.  (/)  |->  A )  =  (/) )
64, 5mpbi 212 1  |-  ( x  e.  (/)  |->  A )  =  (/)
Colors of variables: wff setvar class
Syntax hints:    = wceq 1438    e. wcel 1869   A.wral 2776   _Vcvv 3082   (/)c0 3763    |-> cmpt 4481    Fn wfn 5595
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-9 1873  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401  ax-sep 4545  ax-nul 4554  ax-pr 4659
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 985  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-eu 2270  df-mo 2271  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-ne 2621  df-ral 2781  df-rex 2782  df-rab 2785  df-v 3084  df-dif 3441  df-un 3443  df-in 3445  df-ss 3452  df-nul 3764  df-if 3912  df-sn 3999  df-pr 4001  df-op 4005  df-br 4423  df-opab 4482  df-mpt 4483  df-id 4767  df-xp 4858  df-rel 4859  df-cnv 4860  df-co 4861  df-dm 4862  df-fun 5602  df-fn 5603
This theorem is referenced by:  oarec  7273  swrd00  12774  swrdlend  12787  repswswrd  12887  0rest  15325  grpinvfval  16701  psgnfval  17138  odfval  17176  odfvalOLD  17179  gsumconst  17564  gsum2dlem2  17600  dprd0  17661  staffval  18072  asclfval  18555  mplcoe1  18686  mplcoe5  18689  coe1fzgsumd  18893  evl1gsumd  18942  gsumfsum  19031  pjfval  19265  mavmul0  19573  submafval  19600  mdetfval  19607  nfimdetndef  19610  mdetfval1  19611  mdet0pr  19613  madufval  19658  madugsum  19664  minmar1fval  19667  cramer0  19711  nmfval  21599  mdegfval  23007  gsumvsca1  28551  gsumvsca2  28552  esumnul  28875  esumrnmpt2  28895  sitg0  29185  mrsubfval  30152  msubfval  30168  elmsubrn  30172  mvhfval  30177  msrfval  30181  poimirlem28  31930  cncfiooicc  37640  itgvol0  37713  stoweidlem9  37737  sge0iunmptlemfi  38091  sge0isum  38105  lincval0  39602
  Copyright terms: Public domain W3C validator