Theorem f0 6755

Description: The empty function. (Contributed by NM, 14-Aug-1999.)

Assertion

Ref	Expression
f0	⊢ ∅:∅⟶𝐴

Proof of Theorem f0

Step	Hyp	Ref	Expression
1		eqid 2761	. . 3 ⊢ ∅ = ∅
2		fn0 6662	. . 3 ⊢ (∅ Fn ∅ ↔ ∅ = ∅)
3	1, 2	mpbir 234	. 2 ⊢ ∅ Fn ∅
4		rn0 5908	. . 3 ⊢ ran ∅ = ∅
5		0ss 4350	. . 3 ⊢ ∅ ⊆ 𝐴
6	4, 5	eqsstri 3977	. 2 ⊢ ran ∅ ⊆ 𝐴
7		df-f 6535	. 2 ⊢ (∅:∅⟶𝐴 ↔ (∅ Fn ∅ ∧ ran ∅ ⊆ 𝐴))
8	3, 6, 7	mpbir2an 724	1 ⊢ ∅:∅⟶𝐴

This proof depends on syntax axioms:   = wceq 1570   ⊆ wss 3899  ∅c0 4279  ran crn 5652   Fn wfn 6526  ⟶wf 6527

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-rn 5662  df-fun 6533  df-fn 6534  df-f 6535

This theorem is used by:  f00  6756  f0bi  6757  f10  6850  map0g  8896  ac6sfi  9259  oif  9508  wrd0  14664  0csh0  14924  ram0  17180  0ssc  17992  0subcat  17993  setc2ohom  18250  cat1lem  18251  gsum0  18853  ga0  19492  0frgp  19973  matunitlindf  22976  ptcmpfi  24112  0met  24665  perfdvf  26203  uhgr0e  29631  uhgr0  29633  griedg0prc  29827  0mplrim  34128  locfinref  34455  poimirlem28  38534  sticksstones11  43174  climlimsupcex  46723  0cnf  46831  dvnprodlem3  46902  sge00  47330  hoidmvlelem3  47551