Theorem fn0 6673

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 6644	. . 3 ⊢ (𝐹 Fn ∅ → Rel 𝐹)
2		fndm 6645	. . 3 ⊢ (𝐹 Fn ∅ → dom 𝐹 = ∅)
3		reldm0 5923	. . . 4 ⊢ (Rel 𝐹 → (𝐹 = ∅ ↔ dom 𝐹 = ∅))
4	3	biimpar 483	. . 3 ⊢ ((Rel 𝐹 ∧ dom 𝐹 = ∅) → 𝐹 = ∅)
5	1, 2, 4	syl2anc 596	. 2 ⊢ (𝐹 Fn ∅ → 𝐹 = ∅)
6		fun0 6608	. . . 4 ⊢ Fun ∅
7		dm0 5915	. . . 4 ⊢ dom ∅ = ∅
8		df-fn 6546	. . . 4 ⊢ (∅ Fn ∅ ↔ (Fun ∅ ∧ dom ∅ = ∅))
9	6, 7, 8	mpbir2an 724	. . 3 ⊢ ∅ Fn ∅
10		fneq1 6633	. . 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 4289  dom cdm 5666  Rel wrel 5671  Fun wfun 6537   Fn wfn 6538

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 2148  ax-9 2156  ax-ext 2738  ax-sep 5262  ax-nul 5274  ax-pr 5409

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 2570  df-clab 2745  df-cleq 2758  df-clel 2841  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-br 5115  df-opab 5179  df-id 5561  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-fun 6545  df-fn 6546

This theorem is used by:  mpt0  6684  f0  6766  f00  6767  f0bi  6768  f1o00  6863  fo00  6864  tpos0  8261  ixp0x  8933  0fz1  13590  hashf1  14514  fuchom  18046  grpinvfvi  19080  mulgfval  19166  mulgfvalALT  19167  mulgfvi  19170  0frgp  19880  invrfval  20504  psrvscafval  22135  tmdgsum  24289  deg1fvi  26279  hon0  32182  fconst7v  33002  fnchoice  45790  dvnprodlem3  46703  0funcg2  49903  0funcALT  49907  0fucterm  50362