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 2761	. . 3 ⊢ ∅ = ∅
2		fn0 6648	. . 3 ⊢ (∅ Fn ∅ ↔ ∅ = ∅)
3	1, 2	mpbir 233	. 2 ⊢ ∅ Fn ∅
4		rn0 5900	. . 3 ⊢ ran ∅ = ∅
5		0ss 4353	. . 3 ⊢ ∅ ⊆ 𝐴
6	4, 5	eqsstri 3982	. 2 ⊢ ran ∅ ⊆ 𝐴
7		df-f 6521	. 2 ⊢ (∅:∅⟶𝐴 ↔ (∅ Fn ∅ ∧ ran ∅ ⊆ 𝐴))
8	3, 6, 7	mpbir2an 721	1 ⊢ ∅:∅⟶𝐴

Syntax hints:   = wceq 1559   ⊆ wss 3904  ∅c0 4285  ran crn 5646   Fn wfn 6512  ⟶wf 6513

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-sep 5245  ax-nul 5255  ax-pr 5389

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-mo 2565  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4480  df-sn 4582  df-pr 4584  df-op 4588  df-br 5100  df-opab 5162  df-id 5540  df-xp 5651  df-rel 5652  df-cnv 5653  df-co 5654  df-dm 5655  df-rn 5656  df-fun 6519  df-fn 6520  df-f 6521

This theorem is referenced by:  f00  6742  f0bi  6743  f10  6836  map0g  8862  ac6sfi  9224  oif  9475  wrd0  14549  0csh0  14803  ram0  17041  0ssc  17853  0subcat  17854  setc2ohom  18111  cat1lem  18112  gsum0  18701  ga0  19321  0frgp  19802  ptcmpfi  23853  0met  24406  perfdvf  25945  uhgr0e  29218  uhgr0  29220  griedg0prc  29411  0mplrim  33772  locfinref  34099  matunitlindf  38081  poimirlem28  38111  sticksstones11  42737  climlimsupcex  46307  0cnf  46415  dvnprodlem3  46486  sge00  46914  hoidmvlelem3  47135