Theorem mpt0 6710

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

Syntax hints:   = wceq 1540   ∈ wcel 2108  ∀wral 3061  Vcvv 3480  ∅c0 4333   ↦ cmpt 5225   Fn wfn 6556

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-fun 6563  df-fn 6564

This theorem is referenced by:  oarec  8600  swrd00  14682  swrdlend  14691  repswswrd  14822  0rest  17474  grpinvfval  18996  grpinvfvalALT  18997  mulgnn0gsum  19098  psgnfval  19518  odfval  19550  odfvalALT  19551  gsumconst  19952  gsum2dlem2  19989  dprd0  20051  staffval  20842  gsumfsum  21452  pjfval  21726  asclfval  21899  mplcoe1  22055  mplcoe5  22058  coe1fzgsumd  22308  evl1gsumd  22361  mavmul0  22558  submafval  22585  mdetfval  22592  nfimdetndef  22595  mdetfval1  22596  mdet0pr  22598  madufval  22643  madugsum  22649  minmar1fval  22652  cramer0  22696  nmfval  24601  mdegfval  26101  of0r  32688  mptiffisupp  32702  gsumvsca1  33232  gsumvsca2  33233  elrgspnlem4  33249  esumnul  34049  esumrnmpt2  34069  sitg0  34348  mrsubfval  35513  msubfval  35529  elmsubrn  35533  mvhfval  35538  msrfval  35542  matunitlindflem1  37623  matunitlindf  37625  poimirlem28  37655  evl1gprodd  42118  idomnnzgmulnz  42134  deg1gprod  42141  sticksstones11  42157  liminf0  45808  cncfiooicc  45909  itgvol0  45983  stoweidlem9  46024  sge0iunmptlemfi  46428  sge0isum  46442  lincval0  48332