Theorem fn0 6667

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 6638	. . 3 ⊢ (𝐹 Fn ∅ → Rel 𝐹)
2		fndm 6639	. . 3 ⊢ (𝐹 Fn ∅ → dom 𝐹 = ∅)
3		reldm0 5916	. . . 4 ⊢ (Rel 𝐹 → (𝐹 = ∅ ↔ dom 𝐹 = ∅))
4	3	biimpar 483	. . 3 ⊢ ((Rel 𝐹 ∧ dom 𝐹 = ∅) → 𝐹 = ∅)
5	1, 2, 4	syl2anc 596	. 2 ⊢ (𝐹 Fn ∅ → 𝐹 = ∅)
6		fun0 6602	. . . 4 ⊢ Fun ∅
7		dm0 5908	. . . 4 ⊢ dom ∅ = ∅
8		df-fn 6540	. . . 4 ⊢ (∅ Fn ∅ ↔ (Fun ∅ ∧ dom ∅ = ∅))
9	6, 7, 8	mpbir2an 724	. . 3 ⊢ ∅ Fn ∅
10		fneq1 6627	. . 3 ⊢ (𝐹 = ∅ → (𝐹 Fn ∅ ↔ ∅ Fn ∅))
11	9, 10	mpbiri 261	. 2 ⊢ (𝐹 = ∅ → 𝐹 Fn ∅)
12	5, 11	impbii 212	1 ⊢ (𝐹 Fn ∅ ↔ 𝐹 = ∅)

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570  ∅c0 4282  dom cdm 5659  Rel wrel 5664  Fun wfun 6531   Fn wfn 6532

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pr 5402

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-mo 2566  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-br 5108  df-opab 5172  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-fun 6539  df-fn 6540

This theorem is used by:  mpt0  6678  f0  6760  f00  6761  f0bi  6762  f1o00  6857  fo00  6858  tpos0  8258  ixp0x  8937  0fz1  13602  hashf1  14526  fuchom  18059  grpinvfvi  19112  mulgfval  19198  mulgfvalALT  19199  mulgfvi  19202  0frgp  19912  invrfval  20536  psrvscafval  22169  tmdgsum  24327  deg1fvi  26317  hon0  32282  fconst7v  33101  fnchoice  45871  dvnprodlem3  46784  0funcg2  50018  0funcALT  50022  0fucterm  50477