Theorem mpt0 6605

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

Syntax hints:   = wceq 1539   ∈ wcel 2104  ∀wral 3062  Vcvv 3437  ∅c0 4262   ↦ cmpt 5164   Fn wfn 6453

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2707  ax-sep 5232  ax-nul 5239  ax-pr 5361

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2887  df-ral 3063  df-rex 3072  df-rab 3306  df-v 3439  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-sn 4566  df-pr 4568  df-op 4572  df-br 5082  df-opab 5144  df-mpt 5165  df-id 5500  df-xp 5606  df-rel 5607  df-cnv 5608  df-co 5609  df-dm 5610  df-fun 6460  df-fn 6461

This theorem is referenced by:  oarec  8424  swrd00  14406  swrdlend  14415  repswswrd  14546  0rest  17189  grpinvfval  18667  grpinvfvalALT  18668  mulgnn0gsum  18759  psgnfval  19157  odfval  19189  odfvalALT  19190  gsumconst  19584  gsum2dlem2  19621  dprd0  19683  staffval  20156  gsumfsum  20714  pjfval  20962  asclfval  21132  mplcoe1  21287  mplcoe5  21290  coe1fzgsumd  21522  evl1gsumd  21572  mavmul0  21750  submafval  21777  mdetfval  21784  nfimdetndef  21787  mdetfval1  21788  mdet0pr  21790  madufval  21835  madugsum  21841  minmar1fval  21844  cramer0  21888  nmfval  23793  mdegfval  25276  gsumvsca1  31528  gsumvsca2  31529  esumnul  32065  esumrnmpt2  32085  sitg0  32362  mrsubfval  33519  msubfval  33535  elmsubrn  33539  mvhfval  33544  msrfval  33548  matunitlindflem1  35821  matunitlindf  35823  poimirlem28  35853  sticksstones11  40312  liminf0  43563  cncfiooicc  43664  itgvol0  43738  stoweidlem9  43779  sge0iunmptlemfi  44181  sge0isum  44195  lincval0  46000