Theorem mpt0 6673

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

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2145  ∀wral 3077  Vcvv 3451  ∅c0 4279   ↦ cmpt 5186   Fn wfn 6526

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-fun 6533  df-fn 6534

This theorem is used by:  oarec  8554  swrd00  14772  swrdlend  14783  repswswrd  14915  0rest  17580  grpinvfval  19169  grpinvfvalALT  19170  mulgnn0gsum  19270  psgnfval  19694  odfval  19726  odfvalALT  19727  gsumconst  20128  gsum2dlem2  20165  dprd0  20227  staffval  21078  gsumfsum  21720  pjfval  21992  asclfval  22166  mplcoe1  22326  mplcoe5  22329  coe1fzgsumd  22602  evl1gsumd  22655  mavmul0  22847  submafval  22874  mdetfval  22881  nfimdetndef  22884  mdetfval1  22885  mdet0pr  22887  madufval  22932  madugsum  22938  minmar1fval  22941  matunitlindflem1  22974  matunitlindf  22976  cramer0  22988  nmfval  24887  mdegfval  26360  of0r  33255  mptiffisupp  33268  suppgsumssiun  33615  gsumvsca1  33769  gsumvsca2  33770  elrgspnlem4  33788  domnprodeq0  33822  deg1prod  34097  ply1coedeg  34103  0mplrim  34128  psrgsum  34162  psrmonprod  34166  vieta  34194  esumnul  34662  esumrnmpt2  34682  sitg0  34961  mrsubfval  36242  msubfval  36258  elmsubrn  36262  mvhfval  36267  msrfval  36271  poimirlem28  38534  evl1gprodd  43135  idomnnzgmulnz  43151  deg1gprod  43158  sticksstones11  43174  liminf0  46747  cncfiooicc  46848  itgvol0  46922  stoweidlem9  46963  sge0iunmptlemfi  47367  sge0isum  47381  lincval0  49471  lmdfval  50701  cmdfval  50702