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

Theorem mpt0 6483
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 2819 . . . 4 (𝑥 ∈ ∅ ↦ 𝐴) = (𝑥 ∈ ∅ ↦ 𝐴)
32fnmpt 6481 . . 3 (∀𝑥 ∈ ∅ 𝐴 ∈ V → (𝑥 ∈ ∅ ↦ 𝐴) Fn ∅)
41, 3ax-mp 5 . 2 (𝑥 ∈ ∅ ↦ 𝐴) Fn ∅
5 fn0 6472 . 2 ((𝑥 ∈ ∅ ↦ 𝐴) Fn ∅ ↔ (𝑥 ∈ ∅ ↦ 𝐴) = ∅)
64, 5mpbi 232 1 (𝑥 ∈ ∅ ↦ 𝐴) = ∅
Colors of variables: wff setvar class
Syntax hints:   = wceq 1530  wcel 2107  wral 3136  Vcvv 3493  c0 4289  cmpt 5137   Fn wfn 6343
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2791  ax-sep 5194  ax-nul 5201  ax-pr 5320
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ral 3141  df-rex 3142  df-rab 3145  df-v 3495  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-nul 4290  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-br 5058  df-opab 5120  df-mpt 5138  df-id 5453  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-fun 6350  df-fn 6351
This theorem is referenced by:  oarec  8180  swrd00  13998  swrdlend  14007  repswswrd  14138  0rest  16695  grpinvfval  18134  grpinvfvalALT  18135  mulgnn0gsum  18226  psgnfval  18620  odfval  18652  odfvalALT  18653  gsumconst  19046  gsum2dlem2  19083  dprd0  19145  staffval  19610  asclfval  20100  mplcoe1  20238  mplcoe5  20241  coe1fzgsumd  20462  evl1gsumd  20512  gsumfsum  20604  pjfval  20842  mavmul0  21153  submafval  21180  mdetfval  21187  nfimdetndef  21190  mdetfval1  21191  mdet0pr  21193  madufval  21238  madugsum  21244  minmar1fval  21247  cramer0  21291  nmfval  23190  mdegfval  24648  gsumvsca1  30847  gsumvsca2  30848  esumnul  31300  esumrnmpt2  31320  sitg0  31597  mrsubfval  32748  msubfval  32764  elmsubrn  32768  mvhfval  32773  msrfval  32777  matunitlindflem1  34880  matunitlindf  34882  poimirlem28  34912  liminf0  42063  cncfiooicc  42166  itgvol0  42242  stoweidlem9  42284  sge0iunmptlemfi  42685  sge0isum  42699  lincval0  44460
  Copyright terms: Public domain W3C validator