Theorem f0 6709

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 6617	. . 3 ⊢ (∅ Fn ∅ ↔ ∅ = ∅)
3	1, 2	mpbir 231	. 2 ⊢ ∅ Fn ∅
4		rn0 5872	. . 3 ⊢ ran ∅ = ∅
5		0ss 4353	. . 3 ⊢ ∅ ⊆ 𝐴
6	4, 5	eqsstri 3984	. 2 ⊢ ran ∅ ⊆ 𝐴
7		df-f 6490	. 2 ⊢ (∅:∅⟶𝐴 ↔ (∅ Fn ∅ ∧ ran ∅ ⊆ 𝐴))
8	3, 6, 7	mpbir2an 711	1 ⊢ ∅:∅⟶𝐴

Syntax hints:   = wceq 1540   ⊆ wss 3905  ∅c0 4286  ran crn 5624   Fn wfn 6481  ⟶wf 6482

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 5238  ax-nul 5248  ax-pr 5374

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 3397  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-br 5096  df-opab 5158  df-id 5518  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-fun 6488  df-fn 6489  df-f 6490

This theorem is referenced by:  f00  6710  f0bi  6711  f10  6801  map0g  8818  ac6sfi  9189  oif  9441  wrd0  14464  0csh0  14717  ram0  16952  0ssc  17762  0subcat  17763  setc2ohom  18020  cat1lem  18021  gsum0  18576  ga0  19195  0frgp  19676  ptcmpfi  23716  0met  24270  perfdvf  25820  uhgr0e  29034  uhgr0  29036  griedg0prc  29227  locfinref  33807  matunitlindf  37597  poimirlem28  37627  sticksstones11  42129  climlimsupcex  45751  0cnf  45859  dvnprodlem3  45930  sge00  46358  hoidmvlelem3  46579