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

Theorem mpt0 6484
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 4454 . . 3 𝑥 ∈ ∅ 𝐴 ∈ V
2 eqid 2821 . . . 4 (𝑥 ∈ ∅ ↦ 𝐴) = (𝑥 ∈ ∅ ↦ 𝐴)
32fnmpt 6482 . . 3 (∀𝑥 ∈ ∅ 𝐴 ∈ V → (𝑥 ∈ ∅ ↦ 𝐴) Fn ∅)
41, 3ax-mp 5 . 2 (𝑥 ∈ ∅ ↦ 𝐴) Fn ∅
5 fn0 6473 . 2 ((𝑥 ∈ ∅ ↦ 𝐴) Fn ∅ ↔ (𝑥 ∈ ∅ ↦ 𝐴) = ∅)
64, 5mpbi 231 1 (𝑥 ∈ ∅ ↦ 𝐴) = ∅
Colors of variables: wff setvar class
Syntax hints:   = wceq 1528  wcel 2105  wral 3138  Vcvv 3495  c0 4290  cmpt 5138   Fn wfn 6344
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pr 5321
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3497  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-br 5059  df-opab 5121  df-mpt 5139  df-id 5454  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-fun 6351  df-fn 6352
This theorem is referenced by:  oarec  8178  swrd00  13996  swrdlend  14005  repswswrd  14136  0rest  16693  grpinvfval  18082  grpinvfvalALT  18083  mulgnn0gsum  18174  psgnfval  18559  odfval  18591  odfvalALT  18592  gsumconst  18985  gsum2dlem2  19022  dprd0  19084  staffval  19549  asclfval  20038  mplcoe1  20176  mplcoe5  20179  coe1fzgsumd  20400  evl1gsumd  20450  gsumfsum  20542  pjfval  20780  mavmul0  21091  submafval  21118  mdetfval  21125  nfimdetndef  21128  mdetfval1  21129  mdet0pr  21131  madufval  21176  madugsum  21182  minmar1fval  21185  cramer0  21229  nmfval  23127  mdegfval  24585  gsumvsca1  30782  gsumvsca2  30783  esumnul  31207  esumrnmpt2  31227  sitg0  31504  mrsubfval  32653  msubfval  32669  elmsubrn  32673  mvhfval  32678  msrfval  32682  matunitlindflem1  34770  matunitlindf  34772  poimirlem28  34802  liminf0  41954  cncfiooicc  42057  itgvol0  42133  stoweidlem9  42175  sge0iunmptlemfi  42576  sge0isum  42590  lincval0  44368
  Copyright terms: Public domain W3C validator