Theorem mpt0 6667

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

Syntax hints:   = wceq 1563   ∈ wcel 2145  ∀wral 3079  Vcvv 3457  ∅c0 4288   ↦ cmpt 5186   Fn wfn 6520

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-sep 5251  ax-nul 5261  ax-pr 5395

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-br 5106  df-opab 5168  df-mpt 5187  df-id 5547  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-fun 6527  df-fn 6528

This theorem is referenced by:  oarec  8535  swrd00  14672  swrdlend  14681  repswswrd  14811  0rest  17472  grpinvfval  19035  grpinvfvalALT  19036  mulgnn0gsum  19137  psgnfval  19561  odfval  19593  odfvalALT  19594  gsumconst  19995  gsum2dlem2  20032  dprd0  20094  staffval  20913  gsumfsum  21544  pjfval  21816  asclfval  21988  mplcoe1  22148  mplcoe5  22151  coe1fzgsumd  22425  evl1gsumd  22478  mavmul0  22670  submafval  22697  mdetfval  22704  nfimdetndef  22707  mdetfval1  22708  mdet0pr  22710  madufval  22755  madugsum  22761  minmar1fval  22764  cramer0  22808  nmfval  24706  mdegfval  26180  of0r  32936  mptiffisupp  32950  suppgsumssiun  33305  gsumvsca1  33459  gsumvsca2  33460  elrgspnlem4  33478  domnprodeq0  33512  deg1prod  33790  ply1coedeg  33796  0mplrim  33821  psrgsum  33855  psrmonprod  33859  vieta  33887  esumnul  34355  esumrnmpt2  34375  sitg0  34653  mrsubfval  35871  msubfval  35887  elmsubrn  35891  mvhfval  35896  msrfval  35900  matunitlindflem1  38127  matunitlindf  38129  poimirlem28  38159  evl1gprodd  42746  idomnnzgmulnz  42762  deg1gprod  42769  sticksstones11  42785  liminf0  46365  cncfiooicc  46466  itgvol0  46540  stoweidlem9  46581  sge0iunmptlemfi  46985  sge0isum  46999  lincval0  49046  lmdfval  50278  cmdfval  50279