Theorem mpt0 6678

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

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2145  ∀wral 3078  Vcvv 3453  ∅c0 4282   ↦ cmpt 5190   Fn wfn 6532

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 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pr 5402

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 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-br 5108  df-opab 5172  df-mpt 5191  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-fun 6539  df-fn 6540

This theorem is used by:  oarec  8553  swrd00  14716  swrdlend  14727  repswswrd  14859  0rest  17520  grpinvfval  19108  grpinvfvalALT  19109  mulgnn0gsum  19209  psgnfval  19633  odfval  19665  odfvalALT  19666  gsumconst  20067  gsum2dlem2  20104  dprd0  20166  staffval  21013  gsumfsum  21653  pjfval  21925  asclfval  22099  mplcoe1  22259  mplcoe5  22262  coe1fzgsumd  22535  evl1gsumd  22588  mavmul0  22780  submafval  22807  mdetfval  22814  nfimdetndef  22817  mdetfval1  22818  mdet0pr  22820  madufval  22865  madugsum  22871  minmar1fval  22874  matunitlindflem1  22907  matunitlindf  22909  cramer0  22921  nmfval  24820  mdegfval  26294  of0r  33160  mptiffisupp  33173  suppgsumssiun  33520  gsumvsca1  33674  gsumvsca2  33675  elrgspnlem4  33693  domnprodeq0  33727  deg1prod  34001  ply1coedeg  34007  0mplrim  34032  psrgsum  34066  psrmonprod  34070  vieta  34098  esumnul  34566  esumrnmpt2  34586  sitg0  34865  mrsubfval  36095  msubfval  36111  elmsubrn  36115  mvhfval  36120  msrfval  36124  poimirlem28  38405  evl1gprodd  42991  idomnnzgmulnz  43007  deg1gprod  43014  sticksstones11  43030  liminf0  46629  cncfiooicc  46730  itgvol0  46804  stoweidlem9  46845  sge0iunmptlemfi  47249  sge0isum  47263  lincval0  49353  lmdfval  50583  cmdfval  50584