Theorem mpt0 6663

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

Syntax hints:   = wceq 1540   ∈ wcel 2109  ∀wral 3045  Vcvv 3450  ∅c0 4299   ↦ cmpt 5191   Fn wfn 6509

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-fun 6516  df-fn 6517

This theorem is referenced by:  oarec  8529  swrd00  14616  swrdlend  14625  repswswrd  14756  0rest  17399  grpinvfval  18917  grpinvfvalALT  18918  mulgnn0gsum  19019  psgnfval  19437  odfval  19469  odfvalALT  19470  gsumconst  19871  gsum2dlem2  19908  dprd0  19970  staffval  20757  gsumfsum  21358  pjfval  21622  asclfval  21795  mplcoe1  21951  mplcoe5  21954  coe1fzgsumd  22198  evl1gsumd  22251  mavmul0  22446  submafval  22473  mdetfval  22480  nfimdetndef  22483  mdetfval1  22484  mdet0pr  22486  madufval  22531  madugsum  22537  minmar1fval  22540  cramer0  22584  nmfval  24483  mdegfval  25974  of0r  32609  mptiffisupp  32623  gsumvsca1  33186  gsumvsca2  33187  elrgspnlem4  33203  esumnul  34045  esumrnmpt2  34065  sitg0  34344  mrsubfval  35502  msubfval  35518  elmsubrn  35522  mvhfval  35527  msrfval  35531  matunitlindflem1  37617  matunitlindf  37619  poimirlem28  37649  evl1gprodd  42112  idomnnzgmulnz  42128  deg1gprod  42135  sticksstones11  42151  liminf0  45798  cncfiooicc  45899  itgvol0  45973  stoweidlem9  46014  sge0iunmptlemfi  46418  sge0isum  46432  lincval0  48408  lmdfval  49642  cmdfval  49643