Theorem mpt0 6182

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 4220	. . 3 ⊢ ∀𝑥 ∈ ∅ 𝐴 ∈ V
2		eqid 2760	. . . 4 ⊢ (𝑥 ∈ ∅ ↦ 𝐴) = (𝑥 ∈ ∅ ↦ 𝐴)
3	2	fnmpt 6181	. . 3 ⊢ (∀𝑥 ∈ ∅ 𝐴 ∈ V → (𝑥 ∈ ∅ ↦ 𝐴) Fn ∅)
4	1, 3	ax-mp 5	. 2 ⊢ (𝑥 ∈ ∅ ↦ 𝐴) Fn ∅
5		fn0 6172	. 2 ⊢ ((𝑥 ∈ ∅ ↦ 𝐴) Fn ∅ ↔ (𝑥 ∈ ∅ ↦ 𝐴) = ∅)
6	4, 5	mpbi 220	1 ⊢ (𝑥 ∈ ∅ ↦ 𝐴) = ∅

Syntax hints:   = wceq 1632   ∈ wcel 2139  ∀wral 3050  Vcvv 3340  ∅c0 4058   ↦ cmpt 4881   Fn wfn 6044

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pr 5055

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ral 3055  df-rex 3056  df-rab 3059  df-v 3342  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-br 4805  df-opab 4865  df-mpt 4882  df-id 5174  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-fun 6051  df-fn 6052

This theorem is referenced by:  oarec  7813  swrd00  13637  swrdlend  13651  repswswrd  13751  0rest  16312  grpinvfval  17681  psgnfval  18140  odfval  18172  gsumconst  18554  gsum2dlem2  18590  dprd0  18650  staffval  19069  asclfval  19556  mplcoe1  19687  mplcoe5  19690  coe1fzgsumd  19894  evl1gsumd  19943  gsumfsum  20035  pjfval  20272  mavmul0  20580  submafval  20607  mdetfval  20614  nfimdetndef  20617  mdetfval1  20618  mdet0pr  20620  madufval  20665  madugsum  20671  minmar1fval  20674  cramer0  20718  nmfval  22614  mdegfval  24041  gsumvsca1  30112  gsumvsca2  30113  esumnul  30440  esumrnmpt2  30460  sitg0  30738  mrsubfval  31733  msubfval  31749  elmsubrn  31753  mvhfval  31758  msrfval  31762  matunitlindflem1  33736  matunitlindf  33738  poimirlem28  33768  liminf0  40546  cncfiooicc  40628  itgvol0  40705  stoweidlem9  40747  sge0iunmptlemfi  41151  sge0isum  41165  lincval0  42732