Theorem f0 6789

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

Assertion

Ref	Expression
f0	⊢ ∅:∅⟶𝐴

Proof of Theorem f0

Step	Hyp	Ref	Expression
1		eqid 2734	. . 3 ⊢ ∅ = ∅
2		fn0 6699	. . 3 ⊢ (∅ Fn ∅ ↔ ∅ = ∅)
3	1, 2	mpbir 231	. 2 ⊢ ∅ Fn ∅
4		rn0 5938	. . 3 ⊢ ran ∅ = ∅
5		0ss 4405	. . 3 ⊢ ∅ ⊆ 𝐴
6	4, 5	eqsstri 4029	. 2 ⊢ ran ∅ ⊆ 𝐴
7		df-f 6566	. 2 ⊢ (∅:∅⟶𝐴 ↔ (∅ Fn ∅ ∧ ran ∅ ⊆ 𝐴))
8	3, 6, 7	mpbir2an 711	1 ⊢ ∅:∅⟶𝐴

Syntax hints:   = wceq 1536   ⊆ wss 3962  ∅c0 4338  ran crn 5689   Fn wfn 6557  ⟶wf 6558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-clab 2712  df-cleq 2726  df-clel 2813  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-br 5148  df-opab 5210  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-fun 6564  df-fn 6565  df-f 6566

This theorem is referenced by:  f00  6790  f0bi  6791  f10  6881  map0g  8922  ac6sfi  9317  oif  9567  wrd0  14573  0csh0  14827  ram0  17055  0ssc  17887  0subcat  17888  setc2ohom  18148  cat1lem  18149  gsum0  18709  ga0  19328  0frgp  19811  ptcmpfi  23836  0met  24391  perfdvf  25952  uhgr0e  29102  uhgr0  29104  griedg0prc  29295  locfinref  33801  matunitlindf  37604  poimirlem28  37634  sticksstones11  42137  climlimsupcex  45724  0cnf  45832  dvnprodlem3  45903  sge00  46331  hoidmvlelem3  46552