Theorem fn0 6472

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 6447	. . 3 ⊢ (𝐹 Fn ∅ → Rel 𝐹)
2		fndm 6448	. . 3 ⊢ (𝐹 Fn ∅ → dom 𝐹 = ∅)
3		reldm0 5791	. . . 4 ⊢ (Rel 𝐹 → (𝐹 = ∅ ↔ dom 𝐹 = ∅))
4	3	biimpar 480	. . 3 ⊢ ((Rel 𝐹 ∧ dom 𝐹 = ∅) → 𝐹 = ∅)
5	1, 2, 4	syl2anc 586	. 2 ⊢ (𝐹 Fn ∅ → 𝐹 = ∅)
6		fun0 6412	. . . 4 ⊢ Fun ∅
7		dm0 5783	. . . 4 ⊢ dom ∅ = ∅
8		df-fn 6351	. . . 4 ⊢ (∅ Fn ∅ ↔ (Fun ∅ ∧ dom ∅ = ∅))
9	6, 7, 8	mpbir2an 709	. . 3 ⊢ ∅ Fn ∅
10		fneq1 6437	. . 3 ⊢ (𝐹 = ∅ → (𝐹 Fn ∅ ↔ ∅ Fn ∅))
11	9, 10	mpbiri 260	. 2 ⊢ (𝐹 = ∅ → 𝐹 Fn ∅)
12	5, 11	impbii 211	1 ⊢ (𝐹 Fn ∅ ↔ 𝐹 = ∅)

Syntax hints:   ↔ wb 208   = wceq 1536  ∅c0 4284  dom cdm 5548  Rel wrel 5553  Fun wfun 6342   Fn wfn 6343

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2792  ax-sep 5196  ax-nul 5203  ax-pr 5323

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1084  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-mo 2621  df-eu 2653  df-clab 2799  df-cleq 2813  df-clel 2892  df-nfc 2962  df-ral 3142  df-rex 3143  df-rab 3146  df-v 3493  df-dif 3932  df-un 3934  df-in 3936  df-ss 3945  df-nul 4285  df-if 4461  df-sn 4561  df-pr 4563  df-op 4567  df-br 5060  df-opab 5122  df-id 5453  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-fun 6350  df-fn 6351

This theorem is referenced by:  mpt0  6483  f0  6553  f00  6554  f0bi  6555  f1o00  6642  fo00  6643  tpos0  7915  ixp0x  8483  0fz1  12924  hashf1  13812  fuchom  17226  grpinvfvi  18141  mulgfval  18221  mulgfvalALT  18222  mulgfvi  18225  0frgp  18900  invrfval  19418  psrvscafval  20165  tmdgsum  22698  deg1fvi  24677  hon0  29568  fnchoice  41360  dvnprodlem3  42307