Theorem fn0 6631

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

Syntax hints:   ↔ wb 206   = wceq 1542  ∅c0 4287  dom cdm 5632  Rel wrel 5637  Fun wfun 6494   Fn wfn 6495

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 5243  ax-nul 5253  ax-pr 5379

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 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-fun 6502  df-fn 6503

This theorem is referenced by:  mpt0  6642  f0  6723  f00  6724  f0bi  6725  f1o00  6817  fo00  6818  tpos0  8208  ixp0x  8876  0fz1  13472  hashf1  14392  fuchom  17900  grpinvfvi  18924  mulgfval  19011  mulgfvalALT  19012  mulgfvi  19015  0frgp  19720  invrfval  20337  psrvscafval  21916  tmdgsum  24051  deg1fvi  26058  hon0  31880  fconst7v  32709  fnchoice  45383  dvnprodlem3  46300  0funcg2  49437  0funcALT  49441  0fucterm  49896