Theorem fn0 6662

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 6633	. . 3 ⊢ (𝐹 Fn ∅ → Rel 𝐹)
2		fndm 6634	. . 3 ⊢ (𝐹 Fn ∅ → dom 𝐹 = ∅)
3		reldm0 5910	. . . 4 ⊢ (Rel 𝐹 → (𝐹 = ∅ ↔ dom 𝐹 = ∅))
4	3	biimpar 483	. . 3 ⊢ ((Rel 𝐹 ∧ dom 𝐹 = ∅) → 𝐹 = ∅)
5	1, 2, 4	syl2anc 596	. 2 ⊢ (𝐹 Fn ∅ → 𝐹 = ∅)
6		fun0 6597	. . . 4 ⊢ Fun ∅
7		dm0 5902	. . . 4 ⊢ dom ∅ = ∅
8		df-fn 6534	. . . 4 ⊢ (∅ Fn ∅ ↔ (Fun ∅ ∧ dom ∅ = ∅))
9	6, 7, 8	mpbir2an 724	. . 3 ⊢ ∅ Fn ∅
10		fneq1 6622	. . 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 4279  dom cdm 5651  Rel wrel 5656  Fun wfun 6525   Fn wfn 6526

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 2733  ax-sep 5249  ax-nul 5260  ax-pr 5391

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 2565  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-fun 6533  df-fn 6534

This theorem is used by:  mpt0  6673  f0  6755  f00  6756  f0bi  6757  f1o00  6852  fo00  6853  tpos0  8257  ixp0x  8938  0fz1  13657  hashf1  14582  fuchom  18119  grpinvfvi  19173  mulgfval  19259  mulgfvalALT  19260  mulgfvi  19263  0frgp  19973  invrfval  20599  psrvscafval  22236  tmdgsum  24394  deg1fvi  26383  hon0  32377  fconst7v  33196  fnchoice  45989  dvnprodlem3  46902  0funcg2  50136  0funcALT  50140  0fucterm  50595