Theorem mpt0 6679

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

Syntax hints:   = wceq 1570   ∈ wcel 2143  ∀wral 3079  Vcvv 3455  ∅c0 4287   ↦ cmpt 5193   Fn wfn 6533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5258  ax-nul 5270  ax-pr 5406

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-br 5111  df-opab 5175  df-mpt 5194  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-fun 6540  df-fn 6541

This theorem is referenced by:  oarec  8548  swrd00  14684  swrdlend  14693  repswswrd  14823  0rest  17483  grpinvfval  19046  grpinvfvalALT  19047  mulgnn0gsum  19147  psgnfval  19571  odfval  19603  odfvalALT  19604  gsumconst  20005  gsum2dlem2  20042  dprd0  20104  staffval  20925  gsumfsum  21565  pjfval  21837  asclfval  22009  mplcoe1  22169  mplcoe5  22172  coe1fzgsumd  22445  evl1gsumd  22498  mavmul0  22690  submafval  22717  mdetfval  22724  nfimdetndef  22727  mdetfval1  22728  mdet0pr  22730  madufval  22775  madugsum  22781  minmar1fval  22784  cramer0  22828  nmfval  24726  mdegfval  26200  of0r  33002  mptiffisupp  33016  suppgsumssiun  33370  gsumvsca1  33524  gsumvsca2  33525  elrgspnlem4  33543  domnprodeq0  33577  deg1prod  33851  ply1coedeg  33857  0mplrim  33882  psrgsum  33916  psrmonprod  33920  vieta  33948  esumnul  34416  esumrnmpt2  34436  sitg0  34714  mrsubfval  35978  msubfval  35994  elmsubrn  35998  mvhfval  36003  msrfval  36007  matunitlindflem1  38245  matunitlindf  38247  poimirlem28  38277  evl1gprodd  42862  idomnnzgmulnz  42878  deg1gprod  42885  sticksstones11  42901  liminf0  46487  cncfiooicc  46588  itgvol0  46662  stoweidlem9  46703  sge0iunmptlemfi  47107  sge0isum  47121  lincval0  49172  lmdfval  50404  cmdfval  50405