Theorem f0 6763

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

Assertion

Ref	Expression
f0	⊢ ∅:∅⟶𝐴

Proof of Theorem f0

Step	Hyp	Ref	Expression
1		eqid 2760	. . 3 ⊢ ∅ = ∅
2		fn0 6670	. . 3 ⊢ (∅ Fn ∅ ↔ ∅ = ∅)
3	1, 2	mpbir 234	. 2 ⊢ ∅ Fn ∅
4		rn0 5907	. . 3 ⊢ ran ∅ = ∅
5		0ss 4349	. . 3 ⊢ ∅ ⊆ 𝐴
6	4, 5	eqsstri 3954	. 2 ⊢ ran ∅ ⊆ 𝐴
7		df-f 6542	. 2 ⊢ (∅:∅⟶𝐴 ↔ (∅ Fn ∅ ∧ ran ∅ ⊆ 𝐴))
8	3, 6, 7	mpbir2an 724	1 ⊢ ∅:∅⟶𝐴

This proof depends on syntax axioms:   = wceq 1569   ⊆ wss 3895  ∅c0 4278  ran crn 5651   Fn wfn 6533  ⟶wf 6534

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-mo 2564  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-br 5103  df-opab 5167  df-id 5545  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-fun 6540  df-fn 6541  df-f 6542

This theorem is used by:  f00  6764  f0bi  6765  f10  6858  map0g  8915  ac6sfi  9278  oif  9527  wrd0  14687  0csh0  14948  ram0  17205  0ssc  18017  0subcat  18018  setc2ohom  18275  cat1lem  18276  gsum0  18878  ga0  19517  0frgp  19998  matunitlindf  23001  ptcmpfi  24137  0met  24690  perfdvf  26228  uhgr0e  29654  uhgr0  29656  griedg0prc  29850  0mplrim  34192  locfinref  34519  poimirlem28  38659  sticksstones11  43299  climlimsupcex  46872  0cnf  46980  dvnprodlem3  47051  sge00  47479  hoidmvlelem3  47700