Theorem mpt0 6634

Description: A mapping operation with empty domain. (Contributed by Mario Carneiro, 28-Dec-2014.)

Assertion

Ref	Expression
mpt0	⊢ (𝑥 ∈ ∅ ↦ 𝐴) = ∅

Proof of Theorem mpt0

Step	Hyp	Ref	Expression
1		ral0 4439	. . 3 ⊢ ∀𝑥 ∈ ∅ 𝐴 ∈ V
2		eqid 2737	. . . 4 ⊢ (𝑥 ∈ ∅ ↦ 𝐴) = (𝑥 ∈ ∅ ↦ 𝐴)
3	2	fnmpt 6632	. . 3 ⊢ (∀𝑥 ∈ ∅ 𝐴 ∈ V → (𝑥 ∈ ∅ ↦ 𝐴) Fn ∅)
4	1, 3	ax-mp 5	. 2 ⊢ (𝑥 ∈ ∅ ↦ 𝐴) Fn ∅
5		fn0 6623	. 2 ⊢ ((𝑥 ∈ ∅ ↦ 𝐴) Fn ∅ ↔ (𝑥 ∈ ∅ ↦ 𝐴) = ∅)
6	4, 5	mpbi 230	1 ⊢ (𝑥 ∈ ∅ ↦ 𝐴) = ∅

Syntax hints:   = wceq 1542   ∈ wcel 2114  ∀wral 3052  Vcvv 3430  ∅c0 4274   ↦ cmpt 5167   Fn wfn 6487

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pr 5370

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-fun 6494  df-fn 6495

This theorem is referenced by:  oarec  8490  swrd00  14598  swrdlend  14607  repswswrd  14737  0rest  17383  grpinvfval  18945  grpinvfvalALT  18946  mulgnn0gsum  19047  psgnfval  19466  odfval  19498  odfvalALT  19499  gsumconst  19900  gsum2dlem2  19937  dprd0  19999  staffval  20809  gsumfsum  21424  pjfval  21696  asclfval  21868  mplcoe1  22025  mplcoe5  22028  coe1fzgsumd  22279  evl1gsumd  22332  mavmul0  22527  submafval  22554  mdetfval  22561  nfimdetndef  22564  mdetfval1  22565  mdet0pr  22567  madufval  22612  madugsum  22618  minmar1fval  22621  cramer0  22665  nmfval  24563  mdegfval  26037  of0r  32767  mptiffisupp  32781  suppgsumssiun  33148  gsumvsca1  33302  gsumvsca2  33303  elrgspnlem4  33321  domnprodeq0  33352  deg1prod  33658  ply1coedeg  33664  psrgsum  33707  psrmonprod  33711  vieta  33739  esumnul  34208  esumrnmpt2  34228  sitg0  34506  mrsubfval  35706  msubfval  35722  elmsubrn  35726  mvhfval  35731  msrfval  35735  matunitlindflem1  37951  matunitlindf  37953  poimirlem28  37983  evl1gprodd  42570  idomnnzgmulnz  42586  deg1gprod  42593  sticksstones11  42609  liminf0  46239  cncfiooicc  46340  itgvol0  46414  stoweidlem9  46455  sge0iunmptlemfi  46859  sge0isum  46873  lincval0  48903  lmdfval  50136  cmdfval  50137