Theorem mpt0 6684

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 4464	. . 3 ⊢ ∀𝑥 ∈ ∅ 𝐴 ∈ V
2		eqid 2766	. . . 4 ⊢ (𝑥 ∈ ∅ ↦ 𝐴) = (𝑥 ∈ ∅ ↦ 𝐴)
3	2	fnmpt 6682	. . 3 ⊢ (∀𝑥 ∈ ∅ 𝐴 ∈ V → (𝑥 ∈ ∅ ↦ 𝐴) Fn ∅)
4	1, 3	ax-mp 5	. 2 ⊢ (𝑥 ∈ ∅ ↦ 𝐴) Fn ∅
5		fn0 6673	. 2 ⊢ ((𝑥 ∈ ∅ ↦ 𝐴) Fn ∅ ↔ (𝑥 ∈ ∅ ↦ 𝐴) = ∅)
6	4, 5	mpbi 233	1 ⊢ (𝑥 ∈ ∅ ↦ 𝐴) = ∅

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2146  ∀wral 3082  Vcvv 3458  ∅c0 4289   ↦ cmpt 5197   Fn wfn 6538

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-sep 5262  ax-nul 5274  ax-pr 5409

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-br 5115  df-opab 5179  df-mpt 5198  df-id 5561  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-fun 6545  df-fn 6546

This theorem is used by:  oarec  8556  swrd00  14704  swrdlend  14715  repswswrd  14847  0rest  17507  grpinvfval  19076  grpinvfvalALT  19077  mulgnn0gsum  19177  psgnfval  19601  odfval  19633  odfvalALT  19634  gsumconst  20035  gsum2dlem2  20072  dprd0  20134  staffval  20981  gsumfsum  21621  pjfval  21893  asclfval  22065  mplcoe1  22225  mplcoe5  22228  coe1fzgsumd  22501  evl1gsumd  22554  mavmul0  22746  submafval  22773  mdetfval  22780  nfimdetndef  22783  mdetfval1  22784  mdet0pr  22786  madufval  22831  madugsum  22837  minmar1fval  22840  cramer0  22884  nmfval  24782  mdegfval  26256  of0r  33061  mptiffisupp  33075  suppgsumssiun  33423  gsumvsca1  33577  gsumvsca2  33578  elrgspnlem4  33596  domnprodeq0  33630  deg1prod  33904  ply1coedeg  33910  0mplrim  33935  psrgsum  33969  psrmonprod  33973  vieta  34001  esumnul  34469  esumrnmpt2  34489  sitg0  34767  mrsubfval  36020  msubfval  36036  elmsubrn  36040  mvhfval  36045  msrfval  36049  matunitlindflem1  38307  matunitlindf  38309  poimirlem28  38339  evl1gprodd  42924  idomnnzgmulnz  42940  deg1gprod  42947  sticksstones11  42963  liminf0  46547  cncfiooicc  46648  itgvol0  46722  stoweidlem9  46763  sge0iunmptlemfi  47167  sge0isum  47181  lincval0  49235  lmdfval  50467  cmdfval  50468