Theorem f0 6716

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

Assertion

Ref	Expression
f0	⊢ ∅:∅⟶𝐴

Proof of Theorem f0

Step	Hyp	Ref	Expression
1		eqid 2737	. . 3 ⊢ ∅ = ∅
2		fn0 6624	. . 3 ⊢ (∅ Fn ∅ ↔ ∅ = ∅)
3	1, 2	mpbir 231	. 2 ⊢ ∅ Fn ∅
4		rn0 5876	. . 3 ⊢ ran ∅ = ∅
5		0ss 4353	. . 3 ⊢ ∅ ⊆ 𝐴
6	4, 5	eqsstri 3981	. 2 ⊢ ran ∅ ⊆ 𝐴
7		df-f 6497	. 2 ⊢ (∅:∅⟶𝐴 ↔ (∅ Fn ∅ ∧ ran ∅ ⊆ 𝐴))
8	3, 6, 7	mpbir2an 712	1 ⊢ ∅:∅⟶𝐴

Syntax hints:   = wceq 1542   ⊆ wss 3902  ∅c0 4286  ran crn 5626   Fn wfn 6488  ⟶wf 6489

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5242  ax-nul 5252  ax-pr 5378

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-mo 2540  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3062  df-rab 3401  df-v 3443  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4287  df-if 4481  df-sn 4582  df-pr 4584  df-op 4588  df-br 5100  df-opab 5162  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-fun 6495  df-fn 6496  df-f 6497

This theorem is referenced by:  f00  6717  f0bi  6718  f10  6808  map0g  8826  ac6sfi  9188  oif  9439  wrd0  14466  0csh0  14720  ram0  16954  0ssc  17765  0subcat  17766  setc2ohom  18023  cat1lem  18024  gsum0  18613  ga0  19231  0frgp  19712  ptcmpfi  23761  0met  24314  perfdvf  25864  uhgr0e  29127  uhgr0  29129  griedg0prc  29320  locfinref  33979  matunitlindf  37790  poimirlem28  37820  sticksstones11  42447  climlimsupcex  46049  0cnf  46157  dvnprodlem3  46228  sge00  46656  hoidmvlelem3  46877