Theorem mpt0 6681

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 4453	. . 3 ⊢ ∀𝑥 ∈ ∅ 𝐴 ∈ V
2		eqid 2760	. . . 4 ⊢ (𝑥 ∈ ∅ ↦ 𝐴) = (𝑥 ∈ ∅ ↦ 𝐴)
3	2	fnmpt 6679	. . 3 ⊢ (∀𝑥 ∈ ∅ 𝐴 ∈ V → (𝑥 ∈ ∅ ↦ 𝐴) Fn ∅)
4	1, 3	ax-mp 5	. 2 ⊢ (𝑥 ∈ ∅ ↦ 𝐴) Fn ∅
5		fn0 6670	. 2 ⊢ ((𝑥 ∈ ∅ ↦ 𝐴) Fn ∅ ↔ (𝑥 ∈ ∅ ↦ 𝐴) = ∅)
6	4, 5	mpbi 233	1 ⊢ (𝑥 ∈ ∅ ↦ 𝐴) = ∅

This proof depends on syntax axioms:   = wceq 1569   ∈ wcel 2144  ∀wral 3076  Vcvv 3450  ∅c0 4278   ↦ cmpt 5185   Fn wfn 6533

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5545  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-fun 6540  df-fn 6541

This theorem is used by:  oarec  8573  swrd00  14796  swrdlend  14807  repswswrd  14939  0rest  17605  grpinvfval  19194  grpinvfvalALT  19195  mulgnn0gsum  19295  psgnfval  19719  odfval  19751  odfvalALT  19752  gsumconst  20153  gsum2dlem2  20190  dprd0  20252  staffval  21103  gsumfsum  21745  pjfval  22017  asclfval  22191  mplcoe1  22351  mplcoe5  22354  coe1fzgsumd  22627  evl1gsumd  22680  mavmul0  22872  submafval  22899  mdetfval  22906  nfimdetndef  22909  mdetfval1  22910  mdet0pr  22912  madufval  22957  madugsum  22963  minmar1fval  22966  matunitlindflem1  22999  matunitlindf  23001  cramer0  23013  nmfval  24912  mdegfval  26385  of0r  33320  mptiffisupp  33333  suppgsumssiun  33679  gsumvsca1  33833  gsumvsca2  33834  elrgspnlem4  33852  domnprodeq0  33886  deg1prod  34161  ply1coedeg  34167  0mplrim  34192  psrgsum  34226  psrmonprod  34230  vieta  34258  esumnul  34726  esumrnmpt2  34746  sitg0  35024  mrsubfval  36359  msubfval  36375  elmsubrn  36379  mvhfval  36384  msrfval  36388  poimirlem28  38659  evl1gprodd  43260  idomnnzgmulnz  43276  deg1gprod  43283  sticksstones11  43299  liminf0  46896  cncfiooicc  46997  itgvol0  47071  stoweidlem9  47112  sge0iunmptlemfi  47516  sge0isum  47530  lincval0  49620  lmdfval  50925  cmdfval  50926