Theorem fn0 6309

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 6287	. . 3 ⊢ (𝐹 Fn ∅ → Rel 𝐹)
2		fndm 6288	. . 3 ⊢ (𝐹 Fn ∅ → dom 𝐹 = ∅)
3		reldm0 5641	. . . 4 ⊢ (Rel 𝐹 → (𝐹 = ∅ ↔ dom 𝐹 = ∅))
4	3	biimpar 470	. . 3 ⊢ ((Rel 𝐹 ∧ dom 𝐹 = ∅) → 𝐹 = ∅)
5	1, 2, 4	syl2anc 576	. 2 ⊢ (𝐹 Fn ∅ → 𝐹 = ∅)
6		fun0 6252	. . . 4 ⊢ Fun ∅
7		dm0 5637	. . . 4 ⊢ dom ∅ = ∅
8		df-fn 6191	. . . 4 ⊢ (∅ Fn ∅ ↔ (Fun ∅ ∧ dom ∅ = ∅))
9	6, 7, 8	mpbir2an 698	. . 3 ⊢ ∅ Fn ∅
10		fneq1 6277	. . 3 ⊢ (𝐹 = ∅ → (𝐹 Fn ∅ ↔ ∅ Fn ∅))
11	9, 10	mpbiri 250	. 2 ⊢ (𝐹 = ∅ → 𝐹 Fn ∅)
12	5, 11	impbii 201	1 ⊢ (𝐹 Fn ∅ ↔ 𝐹 = ∅)

Syntax hints:   ↔ wb 198   = wceq 1507  ∅c0 4179  dom cdm 5407  Rel wrel 5412  Fun wfun 6182   Fn wfn 6183

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2751  ax-sep 5060  ax-nul 5067  ax-pr 5186

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2584  df-clab 2760  df-cleq 2772  df-clel 2847  df-nfc 2919  df-ral 3094  df-rex 3095  df-rab 3098  df-v 3418  df-dif 3833  df-un 3835  df-in 3837  df-ss 3844  df-nul 4180  df-if 4351  df-sn 4442  df-pr 4444  df-op 4448  df-br 4930  df-opab 4992  df-id 5312  df-xp 5413  df-rel 5414  df-cnv 5415  df-co 5416  df-dm 5417  df-fun 6190  df-fn 6191

This theorem is referenced by:  mpt0  6320  f0  6389  f00  6390  f0bi  6391  f1o00  6478  fo00  6479  tpos0  7725  ixp0x  8287  0fz1  12743  hashf1  13628  fuchom  17089  grpinvfvi  17933  mulgfval  18013  mulgfvalALT  18014  mulgfvi  18017  symgplusg  18278  0frgp  18665  invrfval  19146  psrvscafval  19884  tmdgsum  22407  deg1fvi  24382  hon0  29351  fnchoice  40702  dvnprodlem3  41661