Theorem mpt0 6640

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

Syntax hints:   = wceq 1542   ∈ wcel 2114  ∀wral 3051  Vcvv 3429  ∅c0 4273   ↦ cmpt 5166   Fn wfn 6493

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-nul 5241  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-br 5086  df-opab 5148  df-mpt 5167  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-fun 6500  df-fn 6501

This theorem is referenced by:  oarec  8497  swrd00  14607  swrdlend  14616  repswswrd  14746  0rest  17392  grpinvfval  18954  grpinvfvalALT  18955  mulgnn0gsum  19056  psgnfval  19475  odfval  19507  odfvalALT  19508  gsumconst  19909  gsum2dlem2  19946  dprd0  20008  staffval  20818  gsumfsum  21414  pjfval  21686  asclfval  21858  mplcoe1  22015  mplcoe5  22018  coe1fzgsumd  22269  evl1gsumd  22322  mavmul0  22517  submafval  22544  mdetfval  22551  nfimdetndef  22554  mdetfval1  22555  mdet0pr  22557  madufval  22602  madugsum  22608  minmar1fval  22611  cramer0  22655  nmfval  24553  mdegfval  26027  of0r  32752  mptiffisupp  32766  suppgsumssiun  33133  gsumvsca1  33287  gsumvsca2  33288  elrgspnlem4  33306  domnprodeq0  33337  deg1prod  33643  ply1coedeg  33649  psrgsum  33692  psrmonprod  33696  vieta  33724  esumnul  34192  esumrnmpt2  34212  sitg0  34490  mrsubfval  35690  msubfval  35706  elmsubrn  35710  mvhfval  35715  msrfval  35719  matunitlindflem1  37937  matunitlindf  37939  poimirlem28  37969  evl1gprodd  42556  idomnnzgmulnz  42572  deg1gprod  42579  sticksstones11  42595  liminf0  46221  cncfiooicc  46322  itgvol0  46396  stoweidlem9  46437  sge0iunmptlemfi  46841  sge0isum  46855  lincval0  48891  lmdfval  50124  cmdfval  50125