Theorem f0 6766

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

Assertion

Ref	Expression
f0	⊢ ∅:∅⟶𝐴

Proof of Theorem f0

Step	Hyp	Ref	Expression
1		eqid 2766	. . 3 ⊢ ∅ = ∅
2		fn0 6673	. . 3 ⊢ (∅ Fn ∅ ↔ ∅ = ∅)
3	1, 2	mpbir 234	. 2 ⊢ ∅ Fn ∅
4		rn0 5921	. . 3 ⊢ ran ∅ = ∅
5		0ss 4360	. . 3 ⊢ ∅ ⊆ 𝐴
6	4, 5	eqsstri 3986	. 2 ⊢ ran ∅ ⊆ 𝐴
7		df-f 6547	. 2 ⊢ (∅:∅⟶𝐴 ↔ (∅ Fn ∅ ∧ ran ∅ ⊆ 𝐴))
8	3, 6, 7	mpbir2an 724	1 ⊢ ∅:∅⟶𝐴

This proof depends on syntax axioms:   = wceq 1570   ⊆ wss 3908  ∅c0 4289  ran crn 5667   Fn wfn 6538  ⟶wf 6539

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-rn 5677  df-fun 6545  df-fn 6546  df-f 6547

This theorem is used by:  f00  6767  f0bi  6768  f10  6861  map0g  8891  ac6sfi  9254  oif  9502  wrd0  14596  0csh0  14856  ram0  17107  0ssc  17919  0subcat  17920  setc2ohom  18177  cat1lem  18178  gsum0  18771  ga0  19399  0frgp  19880  ptcmpfi  24007  0met  24560  perfdvf  26099  uhgr0e  29458  uhgr0  29460  griedg0prc  29651  0mplrim  33935  locfinref  34262  matunitlindf  38310  poimirlem28  38340  sticksstones11  42964  climlimsupcex  46524  0cnf  46632  dvnprodlem3  46703  sge00  47131  hoidmvlelem3  47352