Theorem mpt0 6571

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

Syntax hints:   = wceq 1541   ∈ wcel 2109  ∀wral 3065  Vcvv 3430  ∅c0 4261   ↦ cmpt 5161   Fn wfn 6425

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-10 2140  ax-11 2157  ax-12 2174  ax-ext 2710  ax-sep 5226  ax-nul 5233  ax-pr 5355

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1544  df-fal 1554  df-ex 1786  df-nf 1790  df-sb 2071  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3432  df-dif 3894  df-un 3896  df-in 3898  df-ss 3908  df-nul 4262  df-if 4465  df-sn 4567  df-pr 4569  df-op 4573  df-br 5079  df-opab 5141  df-mpt 5162  df-id 5488  df-xp 5594  df-rel 5595  df-cnv 5596  df-co 5597  df-dm 5598  df-fun 6432  df-fn 6433

This theorem is referenced by:  oarec  8369  swrd00  14338  swrdlend  14347  repswswrd  14478  0rest  17121  grpinvfval  18599  grpinvfvalALT  18600  mulgnn0gsum  18691  psgnfval  19089  odfval  19121  odfvalALT  19122  gsumconst  19516  gsum2dlem2  19553  dprd0  19615  staffval  20088  gsumfsum  20646  pjfval  20894  asclfval  21064  mplcoe1  21219  mplcoe5  21222  coe1fzgsumd  21454  evl1gsumd  21504  mavmul0  21682  submafval  21709  mdetfval  21716  nfimdetndef  21719  mdetfval1  21720  mdet0pr  21722  madufval  21767  madugsum  21773  minmar1fval  21776  cramer0  21820  nmfval  23725  mdegfval  25208  gsumvsca1  31458  gsumvsca2  31459  esumnul  31995  esumrnmpt2  32015  sitg0  32292  mrsubfval  33449  msubfval  33465  elmsubrn  33469  mvhfval  33474  msrfval  33478  matunitlindflem1  35752  matunitlindf  35754  poimirlem28  35784  sticksstones11  40092  liminf0  43288  cncfiooicc  43389  itgvol0  43463  stoweidlem9  43504  sge0iunmptlemfi  43905  sge0isum  43919  lincval0  45708