Theorem mpt0 6642

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

Syntax hints:   = wceq 1542   ∈ wcel 2114  ∀wral 3052  Vcvv 3442  ∅c0 4287   ↦ cmpt 5181   Fn wfn 6495

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-fun 6502  df-fn 6503

This theorem is referenced by:  oarec  8499  swrd00  14580  swrdlend  14589  repswswrd  14719  0rest  17361  grpinvfval  18920  grpinvfvalALT  18921  mulgnn0gsum  19022  psgnfval  19441  odfval  19473  odfvalALT  19474  gsumconst  19875  gsum2dlem2  19912  dprd0  19974  staffval  20786  gsumfsum  21401  pjfval  21673  asclfval  21846  mplcoe1  22004  mplcoe5  22007  coe1fzgsumd  22260  evl1gsumd  22313  mavmul0  22508  submafval  22535  mdetfval  22542  nfimdetndef  22545  mdetfval1  22546  mdet0pr  22548  madufval  22593  madugsum  22599  minmar1fval  22602  cramer0  22646  nmfval  24544  mdegfval  26035  of0r  32768  mptiffisupp  32782  suppgsumssiun  33165  gsumvsca1  33319  gsumvsca2  33320  elrgspnlem4  33338  domnprodeq0  33369  deg1prod  33675  ply1coedeg  33681  psrgsum  33724  psrmonprod  33728  vieta  33756  esumnul  34225  esumrnmpt2  34245  sitg0  34523  mrsubfval  35721  msubfval  35737  elmsubrn  35741  mvhfval  35746  msrfval  35750  matunitlindflem1  37861  matunitlindf  37863  poimirlem28  37893  evl1gprodd  42481  idomnnzgmulnz  42497  deg1gprod  42504  sticksstones11  42520  liminf0  46145  cncfiooicc  46246  itgvol0  46320  stoweidlem9  46361  sge0iunmptlemfi  46765  sge0isum  46779  lincval0  48769  lmdfval  50002  cmdfval  50003