Theorem f0 6749

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

Assertion

Ref	Expression
f0	⊢ ∅:∅⟶𝐴

Proof of Theorem f0

Step	Hyp	Ref	Expression
1		eqid 2765	. . 3 ⊢ ∅ = ∅
2		fn0 6656	. . 3 ⊢ (∅ Fn ∅ ↔ ∅ = ∅)
3	1, 2	mpbir 234	. 2 ⊢ ∅ Fn ∅
4		rn0 5907	. . 3 ⊢ ran ∅ = ∅
5		0ss 4357	. . 3 ⊢ ∅ ⊆ 𝐴
6	4, 5	eqsstri 3985	. 2 ⊢ ran ∅ ⊆ 𝐴
7		df-f 6529	. 2 ⊢ (∅:∅⟶𝐴 ↔ (∅ Fn ∅ ∧ ran ∅ ⊆ 𝐴))
8	3, 6, 7	mpbir2an 723	1 ⊢ ∅:∅⟶𝐴

Syntax hints:   = wceq 1563   ⊆ wss 3907  ∅c0 4288  ran crn 5653   Fn wfn 6520  ⟶wf 6521

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737  ax-sep 5251  ax-nul 5261  ax-pr 5395

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-mo 2569  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-br 5106  df-opab 5168  df-id 5547  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-rn 5663  df-fun 6527  df-fn 6528  df-f 6529

This theorem is referenced by:  f00  6750  f0bi  6751  f10  6844  map0g  8870  ac6sfi  9232  oif  9480  wrd0  14566  0csh0  14820  ram0  17072  0ssc  17884  0subcat  17885  setc2ohom  18142  cat1lem  18143  gsum0  18732  ga0  19359  0frgp  19840  ptcmpfi  23931  0met  24484  perfdvf  26023  uhgr0e  29330  uhgr0  29332  griedg0prc  29523  0mplrim  33821  locfinref  34148  matunitlindf  38129  poimirlem28  38159  sticksstones11  42785  climlimsupcex  46341  0cnf  46449  dvnprodlem3  46520  sge00  46948  hoidmvlelem3  47169