Theorem f0 6760

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

Assertion

Ref	Expression
f0	⊢ ∅:∅⟶𝐴

Proof of Theorem f0

Step	Hyp	Ref	Expression
1		eqid 2762	. . 3 ⊢ ∅ = ∅
2		fn0 6667	. . 3 ⊢ (∅ Fn ∅ ↔ ∅ = ∅)
3	1, 2	mpbir 234	. 2 ⊢ ∅ Fn ∅
4		rn0 5914	. . 3 ⊢ ran ∅ = ∅
5		0ss 4353	. . 3 ⊢ ∅ ⊆ 𝐴
6	4, 5	eqsstri 3980	. 2 ⊢ ran ∅ ⊆ 𝐴
7		df-f 6541	. 2 ⊢ (∅:∅⟶𝐴 ↔ (∅ Fn ∅ ∧ ran ∅ ⊆ 𝐴))
8	3, 6, 7	mpbir2an 724	1 ⊢ ∅:∅⟶𝐴

This proof depends on syntax axioms:   = wceq 1570   ⊆ wss 3902  ∅c0 4282  ran crn 5660   Fn wfn 6532  ⟶wf 6533

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 2734  ax-sep 5255  ax-nul 5267  ax-pr 5402

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 2566  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-br 5108  df-opab 5172  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-fun 6539  df-fn 6540  df-f 6541

This theorem is used by:  f00  6761  f0bi  6762  f10  6855  map0g  8895  ac6sfi  9258  oif  9506  wrd0  14608  0csh0  14868  ram0  17120  0ssc  17932  0subcat  17933  setc2ohom  18190  cat1lem  18191  gsum0  18792  ga0  19431  0frgp  19912  matunitlindf  22909  ptcmpfi  24045  0met  24598  perfdvf  26137  uhgr0e  29536  uhgr0  29538  griedg0prc  29732  0mplrim  34032  locfinref  34359  poimirlem28  38405  sticksstones11  43030  climlimsupcex  46605  0cnf  46713  dvnprodlem3  46784  sge00  47212  hoidmvlelem3  47433