Theorem fn0 6656

Description: A function with empty domain is empty. (Contributed by NM, 15-Apr-1998.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)

Assertion

Ref	Expression
fn0	⊢ (𝐹 Fn ∅ ↔ 𝐹 = ∅)

Proof of Theorem fn0

Step	Hyp	Ref	Expression
1		fnrel 6627	. . 3 ⊢ (𝐹 Fn ∅ → Rel 𝐹)
2		fndm 6628	. . 3 ⊢ (𝐹 Fn ∅ → dom 𝐹 = ∅)
3		reldm0 5908	. . . 4 ⊢ (Rel 𝐹 → (𝐹 = ∅ ↔ dom 𝐹 = ∅))
4	3	biimpar 482	. . 3 ⊢ ((Rel 𝐹 ∧ dom 𝐹 = ∅) → 𝐹 = ∅)
5	1, 2, 4	syl2anc 595	. 2 ⊢ (𝐹 Fn ∅ → 𝐹 = ∅)
6		fun0 6590	. . . 4 ⊢ Fun ∅
7		dm0 5900	. . . 4 ⊢ dom ∅ = ∅
8		df-fn 6528	. . . 4 ⊢ (∅ Fn ∅ ↔ (Fun ∅ ∧ dom ∅ = ∅))
9	6, 7, 8	mpbir2an 723	. . 3 ⊢ ∅ Fn ∅
10		fneq1 6616	. . 3 ⊢ (𝐹 = ∅ → (𝐹 Fn ∅ ↔ ∅ Fn ∅))
11	9, 10	mpbiri 261	. 2 ⊢ (𝐹 = ∅ → 𝐹 Fn ∅)
12	5, 11	impbii 212	1 ⊢ (𝐹 Fn ∅ ↔ 𝐹 = ∅)

Syntax hints:   ↔ wb 209   = wceq 1563  ∅c0 4288  dom cdm 5651  Rel wrel 5656  Fun wfun 6519   Fn wfn 6520

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737  ax-sep 5250  ax-nul 5260  ax-pr 5394

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-mo 2569  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-br 5105  df-opab 5167  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-fun 6527  df-fn 6528

This theorem is referenced by:  mpt0  6667  f0  6749  f00  6750  f0bi  6751  f1o00  6846  fo00  6847  tpos0  8240  ixp0x  8912  0fz1  13560  hashf1  14482  fuchom  18009  grpinvfvi  19037  mulgfval  19123  mulgfvalALT  19124  mulgfvi  19127  0frgp  19837  invrfval  20459  psrvscafval  22055  tmdgsum  24209  deg1fvi  26199  hon0  32050  fconst7v  32873  fnchoice  45608  dvnprodlem3  46521  0funcg2  49714  0funcALT  49718  0fucterm  50173