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 5909	. . . 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 5901	. . . 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 5652  Rel wrel 5657  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 5251  ax-nul 5261  ax-pr 5395

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 5106  df-opab 5168  df-id 5547  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  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  13563  hashf1  14484  fuchom  18011  grpinvfvi  19039  mulgfval  19126  mulgfvalALT  19127  mulgfvi  19130  0frgp  19840  invrfval  20462  psrvscafval  22058  tmdgsum  24213  deg1fvi  26203  hon0  32054  fconst7v  32877  fnchoice  45607  dvnprodlem3  46520  0funcg2  49713  0funcALT  49717  0fucterm  50172