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

Theorem mpt0 6161
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 4217 . . 3 𝑥 ∈ ∅ 𝐴 ∈ V
2 eqid 2771 . . . 4 (𝑥 ∈ ∅ ↦ 𝐴) = (𝑥 ∈ ∅ ↦ 𝐴)
32fnmpt 6160 . . 3 (∀𝑥 ∈ ∅ 𝐴 ∈ V → (𝑥 ∈ ∅ ↦ 𝐴) Fn ∅)
41, 3ax-mp 5 . 2 (𝑥 ∈ ∅ ↦ 𝐴) Fn ∅
5 fn0 6151 . 2 ((𝑥 ∈ ∅ ↦ 𝐴) Fn ∅ ↔ (𝑥 ∈ ∅ ↦ 𝐴) = ∅)
64, 5mpbi 220 1 (𝑥 ∈ ∅ ↦ 𝐴) = ∅
Colors of variables: wff setvar class
Syntax hints:   = wceq 1631  wcel 2145  wral 3061  Vcvv 3351  c0 4063  cmpt 4863   Fn wfn 6026
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4915  ax-nul 4923  ax-pr 5034
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 835  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4226  df-sn 4317  df-pr 4319  df-op 4323  df-br 4787  df-opab 4847  df-mpt 4864  df-id 5157  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-fun 6033  df-fn 6034
This theorem is referenced by:  oarec  7796  swrd00  13626  swrdlend  13640  repswswrd  13740  0rest  16298  grpinvfval  17668  psgnfval  18127  odfval  18159  gsumconst  18541  gsum2dlem2  18577  dprd0  18638  staffval  19057  asclfval  19549  mplcoe1  19680  mplcoe5  19683  coe1fzgsumd  19887  evl1gsumd  19936  gsumfsum  20028  pjfval  20267  mavmul0  20576  submafval  20603  mdetfval  20610  nfimdetndef  20613  mdetfval1  20614  mdet0pr  20616  madufval  20661  madugsum  20667  minmar1fval  20670  cramer0  20716  nmfval  22613  mdegfval  24042  gsumvsca1  30122  gsumvsca2  30123  esumnul  30450  esumrnmpt2  30470  sitg0  30748  mrsubfval  31743  msubfval  31759  elmsubrn  31763  mvhfval  31768  msrfval  31772  matunitlindflem1  33738  matunitlindf  33740  poimirlem28  33770  liminf0  40543  cncfiooicc  40625  itgvol0  40701  stoweidlem9  40743  sge0iunmptlemfi  41147  sge0isum  41161  lincval0  42732
  Copyright terms: Public domain W3C validator