Theorem mpt0 6623

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

Syntax hints:   = wceq 1541   ∈ wcel 2111  ∀wral 3047  Vcvv 3436  ∅c0 4283   ↦ cmpt 5172   Fn wfn 6476

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5234  ax-nul 5244  ax-pr 5370

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4476  df-sn 4577  df-pr 4579  df-op 4583  df-br 5092  df-opab 5154  df-mpt 5173  df-id 5511  df-xp 5622  df-rel 5623  df-cnv 5624  df-co 5625  df-dm 5626  df-fun 6483  df-fn 6484

This theorem is referenced by:  oarec  8477  swrd00  14549  swrdlend  14558  repswswrd  14688  0rest  17330  grpinvfval  18888  grpinvfvalALT  18889  mulgnn0gsum  18990  psgnfval  19410  odfval  19442  odfvalALT  19443  gsumconst  19844  gsum2dlem2  19881  dprd0  19943  staffval  20754  gsumfsum  21369  pjfval  21641  asclfval  21814  mplcoe1  21970  mplcoe5  21973  coe1fzgsumd  22217  evl1gsumd  22270  mavmul0  22465  submafval  22492  mdetfval  22499  nfimdetndef  22502  mdetfval1  22503  mdet0pr  22505  madufval  22550  madugsum  22556  minmar1fval  22559  cramer0  22603  nmfval  24501  mdegfval  25992  of0r  32655  mptiffisupp  32669  gsumvsca1  33190  gsumvsca2  33191  elrgspnlem4  33207  esumnul  34056  esumrnmpt2  34076  sitg0  34354  mrsubfval  35540  msubfval  35556  elmsubrn  35560  mvhfval  35565  msrfval  35569  matunitlindflem1  37655  matunitlindf  37657  poimirlem28  37687  evl1gprodd  42149  idomnnzgmulnz  42165  deg1gprod  42172  sticksstones11  42188  liminf0  45830  cncfiooicc  45931  itgvol0  46005  stoweidlem9  46046  sge0iunmptlemfi  46450  sge0isum  46464  lincval0  48446  lmdfval  49680  cmdfval  49681