Theorem mpt0 6659

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

Syntax hints:   = wceq 1559   ∈ wcel 2141  ∀wral 3075  Vcvv 3453  ∅c0 4285   ↦ cmpt 5180   Fn wfn 6512

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5245  ax-nul 5255  ax-pr 5389

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4480  df-sn 4582  df-pr 4584  df-op 4588  df-br 5100  df-opab 5162  df-mpt 5181  df-id 5540  df-xp 5651  df-rel 5652  df-cnv 5653  df-co 5654  df-dm 5655  df-fun 6519  df-fn 6520

This theorem is referenced by:  oarec  8526  swrd00  14655  swrdlend  14664  repswswrd  14794  0rest  17441  grpinvfval  19003  grpinvfvalALT  19004  mulgnn0gsum  19105  psgnfval  19523  odfval  19555  odfvalALT  19556  gsumconst  19957  gsum2dlem2  19994  dprd0  20056  staffval  20870  gsumfsum  21466  pjfval  21738  asclfval  21910  mplcoe1  22070  mplcoe5  22073  coe1fzgsumd  22347  evl1gsumd  22400  mavmul0  22592  submafval  22619  mdetfval  22626  nfimdetndef  22629  mdetfval1  22630  mdet0pr  22632  madufval  22677  madugsum  22683  minmar1fval  22686  cramer0  22730  nmfval  24628  mdegfval  26102  of0r  32831  mptiffisupp  32845  suppgsumssiun  33213  gsumvsca1  33367  gsumvsca2  33368  elrgspnlem4  33387  domnprodeq0  33421  deg1prod  33740  ply1coedeg  33746  0mplrim  33772  psrgsum  33806  psrmonprod  33810  vieta  33838  esumnul  34306  esumrnmpt2  34326  sitg0  34604  mrsubfval  35822  msubfval  35838  elmsubrn  35842  mvhfval  35847  msrfval  35851  matunitlindflem1  38079  matunitlindf  38081  poimirlem28  38111  evl1gprodd  42698  idomnnzgmulnz  42714  deg1gprod  42721  sticksstones11  42737  liminf0  46331  cncfiooicc  46432  itgvol0  46506  stoweidlem9  46547  sge0iunmptlemfi  46951  sge0isum  46965  lincval0  49001  lmdfval  50234  cmdfval  50235