Theorem fn0 6623

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 6594	. . 3 ⊢ (𝐹 Fn ∅ → Rel 𝐹)
2		fndm 6595	. . 3 ⊢ (𝐹 Fn ∅ → dom 𝐹 = ∅)
3		reldm0 5877	. . . 4 ⊢ (Rel 𝐹 → (𝐹 = ∅ ↔ dom 𝐹 = ∅))
4	3	biimpar 477	. . 3 ⊢ ((Rel 𝐹 ∧ dom 𝐹 = ∅) → 𝐹 = ∅)
5	1, 2, 4	syl2anc 585	. 2 ⊢ (𝐹 Fn ∅ → 𝐹 = ∅)
6		fun0 6557	. . . 4 ⊢ Fun ∅
7		dm0 5869	. . . 4 ⊢ dom ∅ = ∅
8		df-fn 6495	. . . 4 ⊢ (∅ Fn ∅ ↔ (Fun ∅ ∧ dom ∅ = ∅))
9	6, 7, 8	mpbir2an 712	. . 3 ⊢ ∅ Fn ∅
10		fneq1 6583	. . 3 ⊢ (𝐹 = ∅ → (𝐹 Fn ∅ ↔ ∅ Fn ∅))
11	9, 10	mpbiri 258	. 2 ⊢ (𝐹 = ∅ → 𝐹 Fn ∅)
12	5, 11	impbii 209	1 ⊢ (𝐹 Fn ∅ ↔ 𝐹 = ∅)

Syntax hints:   ↔ wb 206   = wceq 1542  ∅c0 4274  dom cdm 5624  Rel wrel 5629  Fun wfun 6486   Fn wfn 6487

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pr 5370

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-mo 2540  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-opab 5149  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-fun 6494  df-fn 6495

This theorem is referenced by:  mpt0  6634  f0  6715  f00  6716  f0bi  6717  f1o00  6809  fo00  6810  tpos0  8199  ixp0x  8867  0fz1  13489  hashf1  14410  fuchom  17922  grpinvfvi  18949  mulgfval  19036  mulgfvalALT  19037  mulgfvi  19040  0frgp  19745  invrfval  20360  psrvscafval  21937  tmdgsum  24070  deg1fvi  26060  hon0  31879  fconst7v  32708  fnchoice  45478  dvnprodlem3  46394  0funcg2  49571  0funcALT  49575  0fucterm  50030