Theorem f0 6741

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

Assertion

Ref	Expression
f0	⊢ ∅:∅⟶𝐴

Proof of Theorem f0

Step	Hyp	Ref	Expression
1		eqid 2729	. . 3 ⊢ ∅ = ∅
2		fn0 6649	. . 3 ⊢ (∅ Fn ∅ ↔ ∅ = ∅)
3	1, 2	mpbir 231	. 2 ⊢ ∅ Fn ∅
4		rn0 5889	. . 3 ⊢ ran ∅ = ∅
5		0ss 4363	. . 3 ⊢ ∅ ⊆ 𝐴
6	4, 5	eqsstri 3993	. 2 ⊢ ran ∅ ⊆ 𝐴
7		df-f 6515	. 2 ⊢ (∅:∅⟶𝐴 ↔ (∅ Fn ∅ ∧ ran ∅ ⊆ 𝐴))
8	3, 6, 7	mpbir2an 711	1 ⊢ ∅:∅⟶𝐴

Syntax hints:   = wceq 1540   ⊆ wss 3914  ∅c0 4296  ran crn 5639   Fn wfn 6506  ⟶wf 6507

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108  df-opab 5170  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-fun 6513  df-fn 6514  df-f 6515

This theorem is referenced by:  f00  6742  f0bi  6743  f10  6833  map0g  8857  ac6sfi  9231  oif  9483  wrd0  14504  0csh0  14758  ram0  16993  0ssc  17799  0subcat  17800  setc2ohom  18057  cat1lem  18058  gsum0  18611  ga0  19230  0frgp  19709  ptcmpfi  23700  0met  24254  perfdvf  25804  uhgr0e  28998  uhgr0  29000  griedg0prc  29191  locfinref  33831  matunitlindf  37612  poimirlem28  37642  sticksstones11  42144  climlimsupcex  45767  0cnf  45875  dvnprodlem3  45946  sge00  46374  hoidmvlelem3  46595