Theorem fn0 6649

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 6620	. . 3 ⊢ (𝐹 Fn ∅ → Rel 𝐹)
2		fndm 6621	. . 3 ⊢ (𝐹 Fn ∅ → dom 𝐹 = ∅)
3		reldm0 5891	. . . 4 ⊢ (Rel 𝐹 → (𝐹 = ∅ ↔ dom 𝐹 = ∅))
4	3	biimpar 477	. . 3 ⊢ ((Rel 𝐹 ∧ dom 𝐹 = ∅) → 𝐹 = ∅)
5	1, 2, 4	syl2anc 584	. 2 ⊢ (𝐹 Fn ∅ → 𝐹 = ∅)
6		fun0 6581	. . . 4 ⊢ Fun ∅
7		dm0 5884	. . . 4 ⊢ dom ∅ = ∅
8		df-fn 6514	. . . 4 ⊢ (∅ Fn ∅ ↔ (Fun ∅ ∧ dom ∅ = ∅))
9	6, 7, 8	mpbir2an 711	. . 3 ⊢ ∅ Fn ∅
10		fneq1 6609	. . 3 ⊢ (𝐹 = ∅ → (𝐹 Fn ∅ ↔ ∅ Fn ∅))
11	9, 10	mpbiri 258	. 2 ⊢ (𝐹 = ∅ → 𝐹 Fn ∅)
12	5, 11	impbii 209	1 ⊢ (𝐹 Fn ∅ ↔ 𝐹 = ∅)

Syntax hints:   ↔ wb 206   = wceq 1540  ∅c0 4296  dom cdm 5638  Rel wrel 5643  Fun wfun 6505   Fn wfn 6506

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-mo 2533  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108  df-opab 5170  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-fun 6513  df-fn 6514

This theorem is referenced by:  mpt0  6660  f0  6741  f00  6742  f0bi  6743  f1o00  6835  fo00  6836  tpos0  8235  ixp0x  8899  0fz1  13505  hashf1  14422  fuchom  17926  grpinvfvi  18914  mulgfval  19001  mulgfvalALT  19002  mulgfvi  19005  0frgp  19709  invrfval  20298  psrvscafval  21857  tmdgsum  23982  deg1fvi  25990  hon0  31722  fnchoice  45023  dvnprodlem3  45946  0funcg2  49073  0funcALT  49077  0fucterm  49532