Theorem f0 6785

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

Assertion

Ref	Expression
f0	⊢ ∅:∅⟶𝐴

Proof of Theorem f0

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

This proof depends on syntax axioms:   = wceq 1570   ⊆ wss 3900  ∅c0 4281  ran crn 5656   Fn wfn 6553  ⟶wf 6554

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5252  ax-nul 5263  ax-pr 5395

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 2102  df-mo 2567  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-br 5107  df-opab 5171  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-fun 6560  df-fn 6561  df-f 6562

This theorem is used by:  f00  6786  f0bi  6787  f10  6881  map0g  8940  ac6sfi  9303  oif  9551  wrd0  14711  0csh0  14972  ram0  17229  0ssc  18041  0subcat  18042  setc2ohom  18299  cat1lem  18300  gsum0  18902  ga0  19542  0frgp  20023  matunitlindf  23026  ptcmpfi  24162  0met  24715  perfdvf  26253  uhgr0e  29679  uhgr0  29681  griedg0prc  29875  0mplrim  34216  locfinref  34543  poimirlem28  38758  sticksstones11  43398  climlimsupcex  46984  0cnf  47092  dvnprodlem3  47163  sge00  47591  hoidmvlelem3  47812