Theorem fn0 6668

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 6639	. . 3 ⊢ (𝐹 Fn ∅ → Rel 𝐹)
2		fndm 6640	. . 3 ⊢ (𝐹 Fn ∅ → dom 𝐹 = ∅)
3		reldm0 5920	. . . 4 ⊢ (Rel 𝐹 → (𝐹 = ∅ ↔ dom 𝐹 = ∅))
4	3	biimpar 482	. . 3 ⊢ ((Rel 𝐹 ∧ dom 𝐹 = ∅) → 𝐹 = ∅)
5	1, 2, 4	syl2anc 595	. 2 ⊢ (𝐹 Fn ∅ → 𝐹 = ∅)
6		fun0 6603	. . . 4 ⊢ Fun ∅
7		dm0 5912	. . . 4 ⊢ dom ∅ = ∅
8		df-fn 6541	. . . 4 ⊢ (∅ Fn ∅ ↔ (Fun ∅ ∧ dom ∅ = ∅))
9	6, 7, 8	mpbir2an 723	. . 3 ⊢ ∅ Fn ∅
10		fneq1 6628	. . 3 ⊢ (𝐹 = ∅ → (𝐹 Fn ∅ ↔ ∅ Fn ∅))
11	9, 10	mpbiri 261	. 2 ⊢ (𝐹 = ∅ → 𝐹 Fn ∅)
12	5, 11	impbii 212	1 ⊢ (𝐹 Fn ∅ ↔ 𝐹 = ∅)

Syntax hints:   ↔ wb 209   = wceq 1570  ∅c0 4287  dom cdm 5663  Rel wrel 5668  Fun wfun 6532   Fn wfn 6533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5258  ax-nul 5270  ax-pr 5406

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-mo 2567  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-br 5111  df-opab 5175  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-fun 6540  df-fn 6541

This theorem is referenced by:  mpt0  6679  f0  6761  f00  6762  f0bi  6763  f1o00  6858  fo00  6859  tpos0  8253  ixp0x  8925  0fz1  13573  hashf1  14496  fuchom  18022  grpinvfvi  19050  mulgfval  19136  mulgfvalALT  19137  mulgfvi  19140  0frgp  19850  invrfval  20472  psrvscafval  22079  tmdgsum  24233  deg1fvi  26223  hon0  32126  fconst7v  32946  fnchoice  45732  dvnprodlem3  46645  0funcg2  49845  0funcALT  49849  0fucterm  50304