Theorem mpt0 6628

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 4466	. . 3 ⊢ ∀𝑥 ∈ ∅ 𝐴 ∈ V
2		eqid 2729	. . . 4 ⊢ (𝑥 ∈ ∅ ↦ 𝐴) = (𝑥 ∈ ∅ ↦ 𝐴)
3	2	fnmpt 6626	. . 3 ⊢ (∀𝑥 ∈ ∅ 𝐴 ∈ V → (𝑥 ∈ ∅ ↦ 𝐴) Fn ∅)
4	1, 3	ax-mp 5	. 2 ⊢ (𝑥 ∈ ∅ ↦ 𝐴) Fn ∅
5		fn0 6617	. 2 ⊢ ((𝑥 ∈ ∅ ↦ 𝐴) Fn ∅ ↔ (𝑥 ∈ ∅ ↦ 𝐴) = ∅)
6	4, 5	mpbi 230	1 ⊢ (𝑥 ∈ ∅ ↦ 𝐴) = ∅

Syntax hints:   = wceq 1540   ∈ wcel 2109  ∀wral 3044  Vcvv 3438  ∅c0 4286   ↦ cmpt 5176   Fn wfn 6481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5238  ax-nul 5248  ax-pr 5374

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5518  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-fun 6488  df-fn 6489

This theorem is referenced by:  oarec  8487  swrd00  14569  swrdlend  14578  repswswrd  14708  0rest  17351  grpinvfval  18875  grpinvfvalALT  18876  mulgnn0gsum  18977  psgnfval  19397  odfval  19429  odfvalALT  19430  gsumconst  19831  gsum2dlem2  19868  dprd0  19930  staffval  20744  gsumfsum  21359  pjfval  21631  asclfval  21804  mplcoe1  21960  mplcoe5  21963  coe1fzgsumd  22207  evl1gsumd  22260  mavmul0  22455  submafval  22482  mdetfval  22489  nfimdetndef  22492  mdetfval1  22493  mdet0pr  22495  madufval  22540  madugsum  22546  minmar1fval  22549  cramer0  22593  nmfval  24492  mdegfval  25983  of0r  32635  mptiffisupp  32649  gsumvsca1  33178  gsumvsca2  33179  elrgspnlem4  33195  esumnul  34014  esumrnmpt2  34034  sitg0  34313  mrsubfval  35480  msubfval  35496  elmsubrn  35500  mvhfval  35505  msrfval  35509  matunitlindflem1  37595  matunitlindf  37597  poimirlem28  37627  evl1gprodd  42090  idomnnzgmulnz  42106  deg1gprod  42113  sticksstones11  42129  liminf0  45775  cncfiooicc  45876  itgvol0  45950  stoweidlem9  45991  sge0iunmptlemfi  46395  sge0isum  46409  lincval0  48401  lmdfval  49635  cmdfval  49636